University of Twente (THE NETHERLANDS)
CADP (Construction and Analysis of Distributed Processes) (BCG and Caesar/Open environments)
LTSmin is a general-purpose toolset for model checking, not tailored
to any particular specification language. It provides reachability
analysis based on BDDs and on a cluster of distributed, enumerative
workstations. It supports specifications in the form of process
algebras (mCRL), state based languages (PROMELA, DVE) and discrete
abstractions of ODE models (MAPLE, GNA). LTSmin also incorporates a
distributed implementation of state space minimization, preserving
strong or branching bisimulation.
LTSmin is designed to be integrated with many other verification tools, both native and general-purpose, notably including CADP. It can export state spaces in the BCG format accepted by CADP, and it implements the Caesar/Open API of CADP, thus providing a direct connection to all on-the-fly model checking and bisimulation tools.
As observed in [Blom-Pol-Weber-10], the modularization software
engineering principle shows its usefulness also in the design of
modern verification tools:
Stefan Blom, Jaco van de Pol, and Michael Weber.
"LTSmin: Distributed and Symbolic Reachability". Proceedings of
the 22th International Conference on Computer Aided Verification
CAV'2010, Lecture Notes in Computer Science vol. 6174, pages 354-359.
Springer Verlag, July 2010.
Available on-line at: http://www.springerlink.com/content/770038851k64gu68/
or from our FTP site in PDF or PostScript
Jaco van de Pol
Department of Computer Science
University of Twente
P.O. Box 217
7500 AE Enschede
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|