Database of Research Tools Developed Using CADP

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 our FTP 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: vdpol@cs.utwente.nl



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Fri Feb 19 09:13:01 2016.


Back to the CADP research tools page