LTSmin Toolset for Manipulating LTSs

Organisation:	University of Twente (THE NETHERLANDS)
Functionality:	Model checking.
Tools used:	CADP (Construction and Analysis of Distributed Processes) (BCG and Caesar/Open environments)
Period:	2010
Description:	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.
Conclusions:	As observed in [Blom-Pol-Weber-10], the modularization software engineering principle shows its usefulness also in the design of modern verification tools: In order to separate specification languages from model checking algorithms, many enumerative, on-the-fly model checkers are based on some next-state interface. It provides transitions between otherwise opaque and monolithic states. For example, the OPEN/CAESAR interface has been underlying the success of the CADP toolkit.
Publications:	[Blom-Pol-Weber-10] 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 the CADP Web site in PDF or PostScript
Contact:	Jaco van de Pol Department of Computer Science University of Twente P.O. Box 217 7500 AE Enschede THE NETHERLANDS Email: [email protected]
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page