Exp.open 2.0: A flexible tool integrating partial order, Compositional, and on-the-fly verification methods

  • Lang F
  • 10


    Mendeley users who have this article in their library.
  • 31


    Citations of this article.


It is desirable to integrate formal verification techniques applicable to different languages. We present EXP.OPEN 2.0, a new tool of the CADP verification toolbox which combines several features. First, EXP.OPEN 2.0 allows to describe concurrent systems as a composition of finite state machines, using either synchronization vectors, or parallel composition, hiding, renaming, and cut operators from several process algebras (CCS, CSP, LOTOS, E-LOTOS, μCRL). Second, together with other tools of CADP, EXP.OPEN 2.0 allows state space generation and on-the-fly exploration. Third, EXP.OPEN 2.0 implements on-the-fly partial order reductions to avoid the generation of irrelevant interleavings of independent transitions. Fourth, EXP.OPEN 2.0 allows to export models towards other tools using interchange formats such as automata networks and Petri nets. Finally, we show some practical applications and measure the efficiency of EXP.OPEN 2.0 on several benchmarks. © Springer-Verlag Berlin Heidelberg 2005.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Frédéric Lang

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free