In this chapter we describe the use of the Kit for checking liveness properties of concurrent systems. There are two steps one has to do, and so this chapter is subdivided into two parts:

• Defining safety and liveness properties
• Checking safety and liveness properties

Defining safety and liveness properties

We specify safety and liveness properties to be checked in terms of temporal logics like CTL and LTL. They are the most popular temporal logics, and together they can express all common safety and liveness properties.
In the following we will restrict our considerations to only a part of CTL's and LTL's syntax, but for a more detailed description of CTL and LTL see here.

• Example 1:

For the system specified in chapter Modelling a system as CFA we are interested in the question if a process trying to access its critical region can do so in finite time. We can express the desired property in LTL in the following way:
G (("trying1" => (F "incs1")) & ("trying2" => (F "incs2")))

For later use we store this formula in a file called liveness_1.ltl.

• Example 2:

In this example we prove the property that process 1 can enter its critical region over and over again, specified as CTL formula. For that, on all paths it must globally hold that there exists a path where it eventually holds that process 1 stays in local state "incs1":
AG EF "incs1"

For later use we write this formula into a file called cr1entry.ctl.

Checking safety and liveness properties

• Example 1:

The Kit offers several algorithms for checking LTL properties, and we show how they are used.

• Using PEP:

To invoke the PEP algorithm type the following line:

check cfa:pep-ltl dekker.cfa liveness_1.ltl

The following output should appear on your screen:

Time needed: 0.180000 seconds
Result: NO.
Counterexample:
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek2: B2 [ flag1=0 --> flag1=0 ] B3
dek1: A1 [ flag1=0 --> flag1=1 ] A2
*** loop starts here ***
dek1: A2 [ flag2=1 --> flag2=1 ] A5
dek1: A5 [ turn=1 --> turn=1 ] A2
*** loop ends here ***

• Using PROD:

Type the following line to use PROD:

check cfa:prod-ltl dekker.cfa liveness_1.ltl

The following output should appear on your screen:

Time needed: 3.330000 seconds
Result: NO.
Counterexample:
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek1: A1 [ flag1=0 --> flag1=1 ] A2
*** loop starts here ***
dek1: A2 [ flag2=1 --> flag2=1 ] A5
dek1: A5 [ turn=1 --> turn=1 ] A2
*** loop ends here ***

• Using SPIN:

Type the following line to use SPIN:

check cfa:spin-ltl dekker.cfa liveness_1.ltl

The following output should appear on your screen:

Time needed: 0.650000 seconds
Result: NO.
Counterexample:
dek2: B1 [ flag2=0 --> flag2=1 ] B2
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek1: A2 [ flag2=1 --> flag2=1 ] A5
dek2: B2 [ flag1=1 --> flag1=1 ] B5
dek2: B5 [ turn=1 --> turn=1 ] B6
dek1: A5 [ turn=1 --> turn=1 ] A2
dek2: B6 [ flag2=1 --> flag2=0 ] B7
dek1: A2 [ flag2=0 --> flag2=0 ] A3
dek1: A3 [ turn=1 --> turn=2 ] A4
dek2: B7 [ turn=2 --> turn=2 ] B8
dek2: B8 [ flag2=0 --> flag2=1 ] B2
dek2: B2 [ flag1=1 --> flag1=1 ] B5
dek1: A4 [ flag1=1 --> flag1=0 ] A1
dek2: B5 [ turn=2 --> turn=2 ] B2
dek1: A1 [ flag1=0 --> flag1=1 ] A2
dek1: A2 [ flag2=1 --> flag2=1 ] A5
dek1: A5 [ turn=2 --> turn=2 ] A6
dek2: B2 [ flag1=1 --> flag1=1 ] B5
dek1: A6 [ flag1=1 --> flag1=0 ] A7
dek2: B5 [ turn=2 --> turn=2 ] B2
*** loop starts here ***
dek1: A7 [ turn=2 --> turn=2 ] A7
*** loop ends here ***

• Using DSSZ:

To invoke the DSSZ algorithm type the following line:

check cfa:dssz-ltl dekker.cfa liveness_1.ltl

The following output should appear on your screen (note that this checker does not produce any counterexamples):

Time needed: 0.210000 seconds
Result: NO.

By means of a counterexample we see that the formula specified above does not hold. This is due to the fact that we do not have considered some fairness conditions. So, if a process can execute a transition, the process should execute this transition in finite time.


Consideration of fairness conditions

We change the specification of the dekker algorithm in such a way that we consider fairness conditions. For the new specification see here.

Now the formula to be checked looks like the following:

(G F "prcs=1" & G F "prcs=2") =>
G (("trying1" => (F "incs1")) & ("trying2" => (F "incs2")))

We write the formula to a file called liveness_2.ltl.

The first part of the formula demands that the automata execute enabled transitions in finite time. So the problem we encountered above (one process may eexecute a loop infinitely often whereas the other process stays in a state for an infinte time although it could execute a transition) can no longer happen.

Now we want to check if this formula holds:

• Using PEP:

check cfa:pep-ltl dekker_fair.cfa liveness_2.ltl

The following output should appear on your screen:

Time needed: 299.730011 seconds
Result: YES.

• Using PROD:

check cfa:prod-ltl dekker_fair.cfa liveness_2.ltl

The following output should appear on your screen:

Time needed: 12.530000 seconds
Result: YES.

• Using SPIN:

check cfa:spin-ltl dekker_fair.cfa liveness_2.ltl

The following output should appear on your screen:

Time needed: 277.800000 seconds
Result: YES.

• Using DSSZ:

check cfa:dssz-ltl dekker_fair.cfa liveness_2.ltl

The following output should appear on your screen:

Time needed: 0.770000 seconds
Result: YES.

 

• Example 2:

The Kit offers several methods for checking CTL formulae, and now we check the property described above with these techniques.

• Using PROD:

check cfa:prod-ctl dekker.cfa cr1entry.ctl

The following output should appear on your screen:

Time needed: 1.940001 seconds
Result: YES.

• Using SMV:

check cfa:smv-ctl dekker.cfa cr1entry.ctl

The following output should appear on your screen:

Time needed: 0.010000 seconds
Result: YES.

• Using DSSZ:

check cfa:dssz-ctl dekker.cfa cr1entry.ctl

The following output should appear on your screen:

Time needed: 0.140000 seconds
Result: YES.