Another interesting task in the verification of concurrent systems is the study of reachability properties (i.e. the question if there exists an execution sequence leading to a state satisfying the property). These properties can be expressed as state formulae and therefore this chapter is structured in two parts:

• Defining a reachability property
• Checking a reachability property

Defining a reachability property

We specify reachability properties to be checked in terms of propositional logic. They yield results about the states of a system and therefore we call them state formulae. State formulae consist of logical operators [negation (!, -), conjunction (&, *), disjunction (|, +), implication (=>)] and atomic propositions. See here for the full description of state formulae.

• Example 1:

First we want to verify a well known reachability property: the mutual exclusion of critical regions for the system specified in the chapter Modelling a system as CFA.
For this example we want to express something like "Does there exist an execution sequence so that automaton dek1 is in the local state 'incs1' while automaton dek2 is in the local state 'incs2' at the same time?". This property violates the mutex property and therefore we expect that such an execution sequence does not exist.

The state formula looks like the following:

"incs1" & "incs2"

For later use we write this formula to a file called mutex.form.

• Example 2:

We change the system in such a way that the mutex property is violated and the state formula mentioned above holds for a global state. The Kit returns an execution sequence leading to a global state violating the mutex property. For the changed specification of the CFA see here.

For later use we write the CFA specification to a file called dekker_non_mutex.cfa.

Checking a reachability property

The Kit offers several algorithms for checking reachability properties. To invoke these methods one has to type:

• Example 1:
• check cfa:pep-reach dekker.cfa mutex.form

The following output should be printed on your screen:

Time needed: 0.050000 seconds
Result: NO.

• check cfa:mcs-reach dekker.cfa mutex.form

The following output should be printed on your screen:

Time needed: 0.010000 seconds
Result: NO.

• check cfa:prod-reach dekker.cfa mutex.form

The following output should be printed on your screen:

Time needed: 1.970000 seconds
Result: NO.

This is the expected result. There is no execution sequence so that automaton dek1 stays in local state "incs1" and automaton dek2 stays in local state "incs2" at the same time.
• Example 2:
• check cfa:pep-reach dekker_non_mutex.cfa mutex.form

The following output should be printed on your screen:

Time needed: 0.050000 seconds
Result: YES.
Witness:
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek1: A2 [ flag2=0 --> flag2=0 ] A3
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek2: B2 [ flag1=1 --> flag1=0 ] B3

• check cfa:mcs-reach dekker_non_mutex.cfa mutex.form

The following output should be printed on your screen:

Time needed: 0.020000 seconds
Result: YES.
Witness:
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek1: A2 [ flag2=0 --> flag2=0 ] A3
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek2: B2 [ flag1=1 --> flag1=0 ] B3

• check cfa:prod-reach dekker_non_mutex.cfa mutex.form

The following output should be printed on your screen:

Time needed: 2.670000 seconds
Result: YES.
Witness:
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek1: A2 [ flag2=0 --> flag2=0 ] A3
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek2: B2 [ flag1=1 --> flag1=1 ] B5
dek2: B5 [ turn=1 --> turn=1 ] B6
dek2: B6 [ flag2=1 --> flag2=0 ] B7
dek1: A3 [ turn=1 --> turn=2 ] A4
dek2: B7 [ turn=2 --> turn=2 ] B8
dek1: A4 [ flag1=1 --> flag1=0 ] A1
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek1: A2 [ flag2=0 --> flag2=0 ] A3
dek2: B8 [ flag2=0 --> flag2=1 ] B2
dek2: B2 [ flag1=1 --> flag1=0 ] B3

This is the expected result. There exists an execution sequence leading to a global state which violates the mutex property.