Weryfikacja wspomagana komputerowo |
For convenience, we recall here the syntax of LTL in promela.
The syntax of LTL in Promela is:
The atoms you can use to form your formulæ include any test expressible in Promela. You can also use as an atom the position of a process. To do that you can put label in your code. For example, let us say that you have a process with pid P containing a label crit, the atom P@crit is true whenever the process with pid P is in the line labelled by crit.
To use this plainly, you may want to declare active processes at the start of the program, as for example, if you started two instances of a process dummy, dummy[0] is the pid of the first one and dummy[1] the one of the second.
You can check one LTL formula at a time in the verification tab of Spin.
An infamous problem that holds since centuries is known as the Syracuse problem. It considers a sequence of integer u such that for every term ui of the sequence if ui is even, ui+1 = ui/2, and if it is odd, ui+1 = 3 × ui + 1.
Collatz has conjectured that whatever u0 you choose, 1 will appear in the sequence. It is not yet proved, yet as far as people have checked (and that goes to very high numbers) it has not been falsified.
An important feature in Promela is the concept of never claim. A never claim is a process that run in parallel with the other, with the constraint that it has to perform one step whenever any other process perform one step. If it reaches its end, the program stops and raise an error. If it cannot execute any step, the program backtracks to test other paths (without raising an error).
It is only used in the verification tab. Only one can be used at a time (by indicating its name like for the ltl formulæ).
It has two main uses:
For example, you can restrict the behaviour to executions in which the variable step is smaller than 10 with the following code:
never stepsmaller {
do
:: step <=10
od;
}
You can check that a variable x is never bigger than 15 with the following code:
never xsmaller {
do
:: x>15 -> break;
od;
}
This code will raise an error if x is bigger than 15 at some point, but not restrict the execution space. You can mix both to obtain a never claim that restrict to executions in which step is smaller than 10 and check that in those case, x is never bigger than 15:
never xsmaller {
do
:: step <= 10 -> if
:: x>15 -> break;
fi;
od;
}
In never claims, you can use special labels starting with accept. If there is an execution passing infinitely often through an accept label, it raises an error.
For example, the following claim raises an error if there is a path for which x is always lower than 40:
never {
acceptblabla: do
:: x<=40
:: else -> break;
od;
do
:: else
od;
}
Notice that in a never claim, you cannot use assignation or other instruction having direct effect on the values of the variables. Besides that, you can use every Promela instruction.
Never claims are the center of Spin verification. Actually, when you verify a LTL formula, Spin translates it into a never claim.
You can as well ask Spin to generate a never claim from a LTL formula, by using the command «spin -f ’formula’» in a terminal. This will generate a claim that will fail if and only if the formula is satisfied. For example, it is useful if you want an execution satisfying an existential formula.
Continue to work with your previous program.
Download the code stepper.pml, and test it. Write the following properties in LTL and in never claims. Compare your results with the output of spin -f ’formula’
Let us now conceive a program to solve a more consequent problem.
G goats and W wolves travelling together come across the Vistula and want to cross it. There is no bridge, but a boat is on the shores. It can welcome L animals at the same time (who can drive the boat, yes. You are not require to explain how they do that). The trouble is that if at any time in the boat or one of the banks there are strictly more wolves than goats, the predator nature of these otherwise nice animals will take over. And we don’t want any casualty.
This document was translated from LATEX by HEVEA.