Parameterized verification is a hard problem. Even more so, if we
consider parameterized systems with non-atomic checks of global
conditions. For example, an agent might check if all participants have
not raised a flag
if for i = 0 ... N-1: b[i] == 0 then goto succ else fail
It turns out that interesting safety properties of prominent mutual exclusion algorithms can be proven by structural properties of the Petri net representation of instances of these algorithms. Using this observation we developed heuristics to find candidates of potential invariants for the parameterized systems from structural properties of instances.
In a second step we employ first-order theorem proving to check if these candidates indeed are inductive invariants of the parameterized system. For this, we rely on CVC4 and Vampire.
We implemented the proving procedure of finite instances, the generalization heuristics, and the first-order verification of the inductive invariants and safety properties in our tool heron.
For example, the following example of a minimal version of Dijkstra's mutual exclusion algorithm can be proven by heron:
local b [false, true] local pc [initial, toloop, loop, break, crit, done] local p [0 - succ(N)] transition pc(P1)=initial -> b(P1)=true, pc(P1)=toloop transition pc(P1)=toloop -> p(P1)=1, pc(P1)=loop transition pc(P1)=loop, p(P1)>N -> pc(P1)=crit transition pc(P1)=loop, p(P1)=0 -> p(P1)=succ(p(P1)), pc(P1)=loop transition pc(P1)=loop, 1<=p(P1), p(P1)<=N, p(P1)=P1 -> p(P1)=succ(p(P1)), pc(P1)=loop transition pc(P1)=loop, 1<=p(P1), p(P1)<=N, b(p(P1))=false -> p(P1)=succ(p(P1)), pc(P1)=loop transition pc(P1)=loop, 1<=p(P1), p(P1)<=N, p(P1)!=P1, b(p(P1))=true -> pc(P1)=break transition pc(P1)=break -> b(P1)=false, pc(P1)=initial transition pc(P1)=crit -> pc(P1)=done transition pc(P1)=done -> b(P1)=false, pc(P1)=initial critical pc(P1)=crit
It is essential for the mutual exclusion property here that for every
two agents at least one has not yet iterated over the other. This fact
corresponds to a trap involving the current value of the program
pc, the value of the variable
the iteration pointer
heron is written in Python. The code is maintained on the GitLab of the TUM.
Since heron is subject to ongoing research the codebase is unstable. Please refer to the artifact for a stable snapshot.
If you have questions regarding heron, please contact Christoph, Mikhail, or Javier.
This project has received funding from the European Research Council (ERC) under the European Unions Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS).