BISIMULATOR: A modular tool for on-the-fly equivalence checking. The equivalence checking problem consists in verifying that a system (e.g., a protocol) matches its abstract specification (e.g., a service) by comparing their Labeled Transition Systems (Ltss) modulo a given equivalence relation. Two approaches are traditionally used to perform equivalence checking: global verification requires to construct the two Ltss before comparison, whereas local (or on-the-fly) verification allows to explore them incrementally during comparison. The latter approach is able to detect errors even in prohibitively large systems, and therefore reveals more effective in combating state explosion.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- 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; Serwe, Wendelin: CADP 2010: a toolbox for the construction and analysis of distributed processes (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)
- Garavel, Hubert; Salaün, Gwen; Serwe, Wendelin: On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP (2009)
- Joubert, Christophe; Mateescu, Radu: Distributed on-the-fly model checking and test case generation (2006)
- Bergamini, Damien; Descoubes, Nicolas; Joubert, Christophe; Mateescu, Radu: BISIMULATOR: A modular tool for on-the-fly equivalence checking (2005)
- Salaün, Gwen; Serwe, Wendelin: Translating hardware process algebras into standard process algebras: Illustration with CHP and LOTOS (2005)