Spin Verification and Specification Modes
After generating a formal model in the Promela language from the Engee environment, the user can verify its correctness using the Spin tool.
The Spin program supports several operating modes that allow you to study the behavior of a model, perform its simulation, and also perform formal verification of specified properties.
This article describes the main Spin modes: simulation and verification, as well as the procedure for adding LTL specifications, generating a verifier, analyzing results, and searching for counterexamples.
The main operating modes of Spin and practical steps for verifying models generated from Engee are described below.
Spin: Simulation mode
Simulation mode allows you to run the model interactively and observe the behavior of the system without checking the formal properties.
For the received path code generation from the Engee model of the Promela file, you can immediately run a simulation of the model using Spin:
spin <имя-файла.pml>If you try to perform this operation with Promela files obtained directly from the Engee code generator, it will lead to endless execution. spin, since the generated Promela model contains an infinite loop.
At the same time, this startup mode spin it can be useful for studying the properties of the model by adding invariants to the source code of Promela (assertions) and operators for generating input data values.
Spin: verification mode
The most useful mode of using the Spin program is the generation of a verifier program. Verification mode is used for strict verification of the logical properties of the model (LTL specifications) and the search for possible errors or contradictions
Verifier is a C program, and its lifecycle consists of supplementing the model text in Promela. by specification, generation and compilation of the verifier program, as well as test programs launches and analyzing messages by the user.
Inserting specifications
The easiest way to transfer the logical formulas of the specification to the Spin program is to add them to the end of the Promela model file in the form of one or more Promela language operators. ltl:
...
описание модели
...
ltl spec_name_1 { ... текст формулы ... }
ltl spec_name_2 { ... текст формулы ... }
...
ltl spec_name_3 { ... текст формулы ... }|
For brevity and clarity logical formulas in front of their list, it may be useful to place C preprocessor directives defining the simple identifiers-abbreviations used in them. For example, formulas can be rewritten as |
|
When defining preprocessor macros, care should be taken not to redefine the identifiers used later in the text. The above example should not start by defining a macro with the name |
Generating and running the verifier
There are two main approaches to generating and running a verifier using the Spin program: combined and separate.
A common prerequisite for the successful execution of the verifier in both cases is the presence of an installed C compiler that supports the ISO C99 standard or higher.
Combined verifier generation and launch
The Spin utility can act as a shell that:
-
Converts
.pml-Promela model file to intermediate files in C language; -
Calls the compiler to translate intermediate C files into a binary executable verifier file named
panand runs it in the model verification mode.
Command line 
for the combined generation and launch mode, it must contain the parameter -run. Example of a command:
spin -run <путь-к-файлу-модели.pml>If the Promela model file contains only one statement ltl, then this command line is enough to run the verification of the formula specified in the operator ltl.
If the Promela model file contains more than one operator ltl, then when running this command line, the formula of the first operator in order will be verified.
To select which of the formulas will be verified at startup spin -run, you should additionally specify the parameter -ltl with the operator’s name ltl.
For example, if the Promela model file has the path ./model.pml and ends with a block of operators.:
ltl spec1 { []a }
ltl spec2 { <>b }That’s a challenge:
spin -run ./model.pmlgenerates and executes the formula verifier []a with a name spec1. And to generate and execute a verifier for the formula <>b with a name spec2, you need to call:
spin -run -ltl spec2 ./model.pmlIn the combined generation and startup mode, Spin does not save intermediate files in the C language. After successful execution of the program, a verifier executable file with the name is automatically created in the current directory. pan (on UNIX-like systems). This file can be used for repeated verifier runs, for example, to check formulas that have not yet been verified.
Separate generation and launch of the verifier
When the Spin program is used in the mode of separate generation and launch of the verifier, its main task is to transform the Promela model into the source code of the C verifier. It is assumed that the user will compile the intermediate C files themselves and run the resulting verifier.
Separate verifier generation
A typical command line for generating the source code of a C verifier:
spin -a <имя модели.pml>Spin does not follow the usual conventions on operating system return codes, so you can only find out whether Spin has completed successfully or with an error by analyzing the text of the program output to the console.
As a result of successful generation, Spin creates or overwrites files with the names pan.c, pan.h, pan.b, pan.m and pan.t (these names are fixed, there is no Spin setting for changing them). At least two of them — pan.c and pan.h — necessary for the next step.
Compiling the verifier
For further translation of the files received in the previous step, a C compiler supporting the ISO C99 standard or higher is required. The command line for compilation may look like this:
cc pan.c -o <результирующий-файл>Or, if the verified formula contains the neXt operator (for more information, see Linear Time Time Logic (LTL) in Spin:
cc -DNXT -DNOREDUCE pan.c -o <результирующий-файл>Launching the verifier
To start the verification session, it is enough to specify the parameter in the command line of the verifier program -a.
An example of a command line when the verifier executable file has the name pan:
./pan -aThe parameters of this command line are sufficient if the Promela model file does not contain operators ltl or it contains only one such operator.
If the operators ltl If there are several formulas, then you need to select the only formula that we are going to verify. To do this, you need to specify the parameter -N with the operator’s name ltl.
For example, if the Promela model file contains the operator ltl spec1 { … }, then verification is performed using the command:
./pan -a -N spec1Analyzing verifier messages
If the verifier verifies the LTL formula of the specification, then information about the success or error of verification should be found in the messages issued by the verifier to the console and starting with the line:
<имя-исполняемого-файла-верификатора>: ltl formula <имя-оператора-ltl>Successful verification
In case of successful verification, if the verifier executable file has a default name pan, and the operator is being verified ltl with a name spec1, then the result of successful verification looks like this:
pan: ltl formula spec1
...
State-vector ... byte, depth reached ..., errors: 0
...Above, you should pay attention to the message errors: n, where n in case of successful verification, it is zero.
Verification error
If verification fails, the output to the console looks like this:
<имя-верификатора>: ltl formula <имя-оператора-ltl>
<имя-верификатора>:1: assertion violated ... (at depth ...)
<имя-верификатора>: wrote <имя-файла-модели>.trail
State-vector ... byte, depth reached ..., errors: 1For example, if the model file name is — model.pml the verifier executable file has a default name pan, and the operator is being verified ltl with a name spec2:
ltl spec2 { []a }the result of the verification error may look like this:
pan: ltl formula spec2
pan:1: assertion violated !( !(a)) (at depth 0)
pan: wrote model.pml.trail
...
State-vector 20 byte, depth reached 5, errors: 1
...Low memory error
In addition, in the case of large models using a large number of variables and/or variables of "wide" types. short or int as a result of the growth of the state space, the verifier may not have enough memory provided to it. In this case, the error may be signaled by messages like:
pan: out of memoryor
error: max search depth too smallIf the latter can be circumvented in some cases by using the parameter -m N For example:
spin -run -m10000000 model.pmlthe first one most often indicates that the model needs to be coarsened, since its state space is too large for analysis using spin.
Finding a counterexample
The console output of the verifier in the example of unsuccessful verification above contains the line:
pan: wrote model.pml.trailThis line indicates that a trace file was created during verification. model.pml.trail.
Using the Spin utility, information can be extracted from the trace file to construct a counterexample, which clearly refutes the verified LTL formula of the specification.
Minimal Spin command line for route analysis:
spin -t -p -g -l -k <имя-файла-трассы.trail> <имя-файла-модели.pml>For example, the model file model.pml contains the text of a simple model:
bool a = true; /* объявление глобальной логической переменной "a",
* инициализированной значением "true"
*/
active proctype fsm() { /* объявление типа процесса "fsm" и его немедленный запуск */
do /* оператор недетерминированного бесконечного цикла */
:: a = true; /* первая возможная ветка цикла */
:: a = false; /* вторая возможная ветка цикла */
od /* окончание оператора цикла */
}
ltl spec1 { []a } /* LTL-формула: "a" истинно всегда */Semantics of the above example in Promela language: global variable a initialized with the value true and then its value randomly changes to false or true.
At the same time, the operator ltl spec1 asserts that the value a must be true for the entire lifetime of the variable. a.
Challenge spin for joint generation and verification in this case, it may look like this:
spin -run -a model.pmlAs a result, you can find the text in the Spin console output.:
pan:1: assertion violated !( !(a)) (at depth 2)
pan: wrote model.pml.trail
...
State-vector 20 byte, depth reached 2, errors: 1
...The first line indicates the name spec1 the operator ltl, the verification of which resulted in an error. The third line contains the name of the route file model.pml.trail, which can be used to generate a counterexample further:
spin -t -k model.pml.trail model.pmlltl spec1: [] (a)
starting claim 1
Never claim moves to line 4 [(1)]
2: proc 0 (fsm:1) model.pml:7 (state 2) [a = 0]
a = 0
spin: _spin_nvr.tmp:3, Error: assertion violated
spin: text of failed assertion: assert(!(!(a)))
Never claim moves to line 3 [assert(!(!(a)))]
spin: trail ends after 3 steps
#processes: 1
a = 0
3: proc 0 (fsm:1) model.pml:5 (state 3)
3: proc - (spec1:1) _spin_nvr.tmp:2 (state 6)
1 processes createdHere, the basic information about the counterexample is contained in the lines:
2: proc 0 (fsm:1) model.pml:7 (state 2) [a = 0]
a = 0
spin: _spin_nvr.tmp:3, Error: assertion violatedIt is shown that the variable a acquires significance false in line 7 of the file model.pml. This is a constructive proof that the model is in its achievable part, where the value a it becomes a lie, and the LTL formula that requires the opposite contradicts each other. To eliminate this contradiction, it is necessary to modify either the model or its specification (operator ltl spec1).