Computer Science Department at ULB   Groupe Verif  

Software


Back to my homepage

Interval Sharing Trees

The IST library is a C library that provides a set of functions together with the IST data structure to manipulate interval constraints (i.e. contraints of the form $ x \in [a,b]$ where $ a \in \mathbb{N}, b \in \mathbb{N}\cup \{ +\infty \}$) in a multi-dimensional space.  More precisely, the sets that can be represented by IST are the sets that can be defined by formulas constructed from the following grammar
$\displaystyle \phi := x \in [a,b] \vert \phi \wedge \phi \vert \neg \phi $
where boolean connectors have the usual semantics.
IST is an extension of the CST (Covering Sharing Trees) [DR00,DRV04] data structure based on the Sharing Tree data structure [Zam97]. CST allows to represent the sets that can be defined by formulas constructed from the following grammar
$\displaystyle \phi := x \in [a,+\infty] \vert \phi \wedge \phi \vert \phi \vee \phi $

Additionally to the traditional operations on sets [GMD+07,Gan02], some useful operations for the verification of discrete systems have been implemented [Van03, Gan02, DRV02]. An example of discrete systems which are handled by the library are models obtained by applying a so-called counting abstraction on abstractions of multi-threaded Java programs. The verification problem that is solved using the library is the coverability problem (a mild form of the reachability problem). We developed some coverability checking tools. More information is given in the section about coverability checkers.


People involved in the development of the Interval Sharing Tree:
  • Pierre Ganty
  • Laurent Van Begin
  • Giorgio Delzanno
  • Jean-François Raskin

    • References

    [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.

    [GVanB07] Pierre Ganty, Laurent Van Begin. Non Deterministic Automata for the Efficient Representation of Infinite-state Systems. Proceedings of CP+CV, 1st workshop on Constraint Programming and Constraints for Verification, Barcelona, Spain, 2004.

    [DR00] Giorgio Delzanno and Jean-François Raskin. Symbolic Representation of Upward-Closed Sets. In the proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'00), Lecture Notes in Computer Science 1785, pages 426--440, Springer, 2000.

    [DRV04] Giorgio Delzanno, Jean-François Raskin and Laurent Van Begin. CSTs (Covering Sharing Trees):  compact Data Structures for Parameterized Verification. Will appear in Software Tools for Technology Transfer manuscript, 2004.

    [Gan02] Pierre Ganty. Algorithmes et structures de données efficaces pour la manipulation de contraintes sur les intervalles. Master's Thesis, Université Libre de Bruxelles, Bruxelles, Belgium, 2002.

    [Zam97] Denis Zampuniéris. The Sharing Tree data structure: Theory and Applications in Formal Verification. Ph.D. Thesis, Facultés Universitaires Notre-Dame de la Paix, Namur, Belgium.

    Coverability Checkers

    On the top of the IST library we have implemented several tools to decide the coverability problem for Petri net and monotonic extensions of the model. The coverability problem is a weaker version of reachability problem. Those tools implements forward/backward search of the state space using a symbolic data structure (the IST library). On top of that, efficient techniques have been implemented to tackle the state explosion problem. Those includes abstraction-refinement techniques [GGVanbR09,GVanbR09] or 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: 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: 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: 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: 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 [Gee07]. (eec is used internally by tsi and ic4pn). More details here.
    The various coverability checkers are described in the following papers:

    References

    [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.

    [Gee07] Gilles Geeraerts. Coverability and Expressiveness Properties of Well-structured Transitions Systems. Ph.D. Thesis, Université Libre de Bruxelles, Bruxelles, Belgium, 2007.

    [Van03] Laurent Van Begin. Efficient Verification of Counting Abstractions for Parametric systems. Ph.D. Thesis, Université Libre de Bruxelles, Bruxelles, Belgium, 2003.

    [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.

    [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.


    Download

    The source code of the coverability checkers is under the GPL license and available here (updated 05-Jun-09).

    Input format

    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

    Remarks
    • 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.

    Example


    Computing the Coverability Set

    If you are interested in computing the coverability set see CSC.


    Back to my homepage
    Updated: Sun Jun 27 23:20:03 CEST 2010
    Copyright © 2010 Pierre Ganty