Home
The coverability checkers implements forward/backward search of the state space using a symbolic data structure called Interval Sharing Tree. The techniques implemented in the various checkers include abstraction-refinement techniques [GGVanbR09,GVanbR09], efficient traversal techniques of the state space [DRV01]. The coverability problem is solved on the Petri net model [DRV01,GGVanbR09,GVanbR09] and on an extension called Multi-Transfers Net (MTN for short) [DRV02]. Petri nets are useful to model a wide range of parametric systems (concurrent systems where the number of process is a priori not known). MTNs allows to model abstractions of multi-threaded Java programs that forget the identity of the threads using a counting abstraction but model precisely the synchronization primitive between threads (notify, notifyall primitives).
There are four different coverability checkers based on various techniques.
-
backward(references to cite [GMD+07,DRV02]): for Petri nets and MTN, backward state space search from the target states, uses places invariant to prune the search. In the above context the algorithm always terminates. The algorithm also handles the case when the target set of states is not upward closed or when the guards of the transitions are not upward closed. However termination is not guaranteed anymore. A detailed description of the algorithm is given in [Gan02,Van03]. -
ic4pn(references to cite [GMD+07,GVanbR09]): for Petri nets only, abstraction refinement algorithm that combines forward and backward state space traversal. The abstraction used in there tries to minimize the dimensionality of the underlying Petri net as described in [GVanbR09]. -
tsi(references to cite [GMD+07,GGVanbR09]): for Petri nets only, abstraction refinement algorithm that combines forward and backward state space traversal. The abstraction tries to minimize the number of predicate used for each place in the Petri net as described in [GGVanbR09]. -
eec(references to cite [GMD+07,GRVanb06]): for Petri nets only, abstraction refinement algorithm that combines forward state space traversal with predicate enumeration. The abstraction tries to minimize the number of predicate used for each place in the Petri net as described in [GRVanb06]. More details here.
[GGVanbR09] Pierre Ganty, Gilles Geeraerts, Jean-François Raskin and Laurent Van Begin. Méthodes algorithmiques pour l'analyse des réseaux de Petri. Journal of Techniques et Sciences Informatiques 28, 2009.
[GVanbR09] Pierre Ganty, Jean-François Raskin and Laurent Van Begin. From Many Places to Few: Automatic Abstraction Refinement for Petri Nets. Invited extended version. Fundamenta Informaticae 88 (3), 275--305, 2008.
[GMD+07] Pierre Ganty, Cédric Meuter, Giorgio Delzanno, Gabriel Kalyon, Jean-François Raskin, Laurent Van Begin. Symbolic Data Structure for sets of k-uples. Technical Report 570, Université Libre de Bruxelles, 2007.
[GRVanb06] Gilles Geeraerts and Jean-François Raskin and Laurent Van Begin. Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS. In the Journal of Computer and System Sciences, 72 (1), pages 180--203, 2006.
[Van03] Laurent Van Begin. Efficient Verification of Counting Abstractions for Parametric systems. Ph.D. Thesis, Université Libre de Bruxelles, Bruxelles, Belgium, 2003.
[DRV02] Giorgio Delzanno, Jean-François Raskin and Laurent Van Begin. Towards the Automated Verification of Multithreaded Java Programs. In the proceedings of the 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'02), Lecture Notes in Computer Science 2280, pages 173--187, Springer, 2002.
[DRV01] Giorgio Delzanno, Jean-François Raskin and Laurent Van Begin. Attacking Symbolic State Explosion. In the proceedings of the 13th International Conference on Computer-aided Verification (CAV'01), Lecture Notes in Computer Science 2102, pages 298--310, Springer, 2001.
# comments S ::= vars set_of_vars rules set_of_rules init init_states target target_states invariants invariant_set set_of_vars::= variable , set_of_vars | variable set_of_rules::= guard -> effect; set_of_rules | epsilon guard ::= guard_atom , guard | guard_atom guard_atom ::= variable >= integer | variable =integer | variable in [integer, integer] effect ::= effect_atom , effect | effect_atom effect_atom ::= variable' = assignment_var assignment_var ::= variable + assignment_var | integer init_states ::= guard init_states | guard target_states ::= guard target_states | guard invariant_set ::= invariant EOL invariant_set | epsilon invariant ::= invariant_atom , invariant | invariant_atom invariant_atom::=variable = integer
- EOL means end of line
- in production rule effect_atom, unless specified otherwise, we assume x'=x+0. Also x+0 can be abbreviated to x
- in production rule effect_atom, the effect that is described must corresponds to a Petri net transition or to a Petri net extension transition (see the references).
- in production rule assignment_var, + followed by - followed by an integer is abbreviated as - followed by an integer. e.g. x' = y+-2 is abbreviated to x'=y-2
- in production rule invariant_atom x=c expresses that, in the equation specifying the invariant, c is the coefficient of variable x.
- CSC, besides including a coverability checker, it computes the coverability set.
- BFC coverability checker, developed in Oxford.
- Petrucchio coverability checker, developed jointly in Oldenburg and Kaiserslautern.
- Safari a model checker designed to prove safety properties of imperative programs with arrays, developed by Francesco Alberti, with contributions from Roberto Bruttomesso.
- Pierre Ganty is the main author, maintainer.
-
Laurent Van Begin (dormant page) provided a first version of the code in
Pascalwhich was then rewritten toC - Pedro Valero provided the regression and benchmarking infrastructure and the plotting infrastructure
- Anthony Piron (dormant page) contributed some of the parsing and error handling code
Maintenance over the years and recent code contributions to Mist were made possible by the financial support of the IMDEA Software Institute.