Skip to content

Examples

We illustrate the use of ProVeLines and its command-line options through several examples. The first step is to compile ProVeLines. For simplicity, disable all the options. In this tutorial, we consider an fPromela model that specifies the behaviour of the minepump examplar of Kramer et al.

First go to the test directory and open minepump.tvl. Eleven boolean features are declared therein. Next, open minepump.pml. We observe that the features data structure includes 7 fields, each of which is a feature declared in minepump.tvl. The others do not occur in the fPromela model. At the beginning of the file, we use #define preprocessor directives to define alias for conditions on the model’s variables. These “derived variables” will be further used to specify properties that the model must satisfy.

Let us now introduce the command-line interface of ProVeLines. Type the following:

$ ./provelines -check ../test/minepump.pml

Then the tool prints:

No never claim, checking only asserts and deadlocks..
No assertion violations or deadlocks found [explored 21177 states, re-explored 229374].

When no property follows the -check option, ProVeLines verifies only the absence of deadlock and assertion violation. The above output reveals that no deadlock occurs in any product. Next, let us verify the property that “it cannot happen that the pump runs indefinitely even though there is methane”, written !<>[] (pumpOn && methane) in LTL. As previously mentioned, pumpOn and methane are derived variables defined by #define preprocessor directives. To verify this property, type the following:

./provelines -check -ltl ‘!<>[] (pumpOn && methane)’ -nt ../test/minepump.pml

The tool prints the following result (partially displayed here):

Checking LTL property !<>[] (pumpOn && methane)..
Property violated [explored 469 states, re-explored 0].
 - Products by which it is violated (as feature expression):
(Start & Stop & MethaneQuery & MethaneAlarm & Low & High)
 - Stack trace:
    …

The above result reveals that the products with the above six features violate the property. By default, ProVeLines stops as soon as it detects a violation. There may exist other products that do not satisfy the property, though. To identify them all, one may use the -exhaustive option:

./provelines -check -ltl ‘!<>[] (pumpOn && methane)’ -exhaustive ../test/minepump.pml
Checking LTL property !<>[] (pumpOn && methane)..
Property violated [explored 469 states, re-explored 0].
- Products by which it is violated (as feature expression):
(Start & Stop & MethaneQuery & MethaneAlarm & Low & High)
- Stack trace:
   …

Property violated [explored 472 states, re-explored 69].
- Products by which it is violated (as feature expression):
(Start & Stop & !MethaneQuery & MethaneAlarm & Low & High)
- Stack trace:
   …

Property violated [explored 6640 states, re-explored 636].
- Products by which it is violated (as feature expression):
(Start & !Stop & MethaneQuery & MethaneAlarm & Low & High)
- Stack trace:
   …

Exhaustive search finished  [explored 13199 states, re-explored 110745].
- 16 problems were found covering the following products (others are ok):
(Start & High)

Once a violation is identified, the corresponding products are excluded from future searches. Hence, two distinct violations cannot refer to the same set of products. ProVeLines displays one counter-example (stack trace) for each found violation. To disable stack trace printing, use -nt option. In the end, the tool displays a formula that represents all the products for which a violation has been found.

It may happen that a property is relevant only to a subset of the products. The -filter option restricts the verification to these products. In the following, we repeat the previous verification, but this time restricted to the products equipped with features Start and Stop:

./provelines -check -ltl ‘!<>[] (pumpOn && methane)’ -filter ‘Start && Stop’ -exhaustive -nt ../test/minepump.pml
Checking LTL property !<>[] (pumpOn && methane)..
Attention! Checks are only done for products satisfying:
  Start && Stop!

Exhaustive search finished  [explored 9614 states, re-explored 18363].
 - 8 problems were found covering the following products (others are ok):
(Start & Stop & High)

ProVeLines ignored the other products during the check, and consequently found fewer violations. This, of course, also reduced the verification time.

Let us now illustrate F-simulation checking. To that aim, we will make use of a variant of the minepump model, minepump_controller2.pml, found in the test directory. In this model, feature High is over-approximated, that is, any product can behave as if it has the feature or not. Now open minepump.prop in the test directory. Two derived variables are written therein, specifying for which properties the simulation will be checked. Go back to the src directory and enter the following command:

./provelines -sim minepump_controller2.pml -props minepump.prop minepump_controller.pml

ProVeLines then checks for which products minepump_controller2.pml simulates minepump_controller.pml. Since the former is an over-approximation of the latter, we expect F-simulation to hold for all the products. After the computation, the tool prints the following:

Checking F-simulation..
Simulation holds for the following products:
All products

This is indeed the expected result. Let us know check whether the converse also holds:

./provelines -sim minepump_controller.pml -props minepump.prop minepump_controller2.pml

The tool prints:

Checking F-simulation..
Simulation holds for the following products:
(!Start) | (Start & High)

Thus, minepump_controller.pml can replicate the behaviour of minepump_controller2.pml only for the products that have feature High. This means that feature High has an actual impact on the properties listed in minepump.prop.

As a last example, we illustrate the verification of real-time models. First compile ProVeLines again after enabling the real-time option in configure.h. Go to test directory and open deadlock-time.pml. Observe that if feature A is enabled, the system will run into a deadlock because the invariant c > 3 has no intersection with the transition guard c < 3. Let us witness that the tool indeed spots this error. Type:

./provelines -check ../test/deadlock-time.pml

As expected, the tool detects the error and outputs the following:

Found deadlock [explored 3 states, re-explored 0].
 - Products by which it is violated (as feature expression):
   (A)

 - Stack trace:
   features                            = All the products
<=0     <=0     \
<INF    <=0     \

   globals.i                           = 0
   globals.c                           = 0
   pid 00, foo                         @ NL13
    --
   features                            = All the products
<=0     <=-3    \
<INF    <=0     \

   pid 00, foo                         @ NL15
    --
   features                            = (A)
<=0     <=-3    \
<INF    <=0     \

   globals.i                           = 1
   pid 00, foo                         @ NL15
    --
    -- Final state repeated in full:
   features                            = (A)
<=0     <=-3    \
<INF    <=0     \

   globals.i                           = 1
   globals.c                           = 0
   pid 00, foo                         @ NL15
    --