Exp.Open 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-The-Fly Verification Methods. 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.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Evrard, Hugues; Lang, Frédéric: Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous (2017)
- Garavel, Hubert; Lang, Frédéric; Mateescu, Radu: Compositional verification of asynchronous concurrent systems using CADP (2015)
- Lang, Frédéric; Mateescu, Radu: Partial model checking using networks of labelled transition systems and Boolean equation systems (2013)
- Garavel, Hubert; Lang, Frédéric; Mateescu, Radu; Serwe, Wendelin: CADP 2010: a toolbox for the construction and analysis of distributed processes (2011)
- Mateescu, Radu; Monteiro, Pedro T.; Dumas, Estelle; de Jong, Hidde: CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks (2011)
- Lang, Frédéric; Salaün, Gwen; Hérilier, Rémi; Kramer, Jeff; Magee, Jeff: Translating FSP into LOTOS and networks of automata (2010)
- Mateescu, Radu; Monteiro, Pedro T.; Dumas, Estelle; de Jong, Hidde: Computation tree regular logic for genetic regulatory networks (2008)
- Lang, Frédéric: Refined interfaces for compositional verification (2006)
- Lang, Frédéric: Exp.Open 2.0: A flexible tool integrating partial order, compositional, and on-the-fly verification methods (2005) ioport
Further publications can be found at: http://cadp.inria.fr/man/exp.open.html#sect33