Abstract Interpretation Toolkit for mCRL

Organisation:	CWI (Amsterdam, THE NETHERLANDS)
Functionality:	Abstract Model Checking
Tools used:	mCRL toolset CADP (Construction and Analysis of Distributed Processes)
Period:	2004
Description:	To reduce the complexity of automatic verification, abstraction based approaches can be used to extract an approximation of the state space that preserves the properties of interest. Given a mCRL specification, the "Abstract Interpretation Toolkit for mCRL" generates both an over- and an under-approximation in the form of an MLTS (modal labelled transition systems), which is represented as a standard labelled transition system using particular labels in order to distinguish between may and must transitions. Formulas are evaluated dually over an MLTS, i.e., there will be a set of states that necessarily satisfy the formula, and a set of states that possibly satisfies the formula. Since a system that necessarily satisfies a formula, also possibly satisfies the formula, satisfaction and refutation of properties are defined via a 3-valued logic, where a formula is either necessarily satisfied, not possibly satisfied, or possibly satisfied but not necessarily satisfied. In practice however, the 3-valued model checking problem is transformed into two standard 2-valued model checking problems, which are then solved by the existing model checker EVALUATOR of CADP.
Conclusions:	The Abstract Interpretation Toolkit for mCRL and EVALUATOR have been successfully experimented in several case studies, such as JavaSpaces http://cadp.inria.fr/case-studies/03-d-javaspaces.html
Publications:	[Pang-vandePol-Espada-04] Jun Pang, Jaco van de Pol, and Miguel Valero Espada. "Abstraction of Parallel Uniform Processes with Data". In Proceedings of the 2nd International Conference on Software Engineering and Formal Methods SEFM'2004 (Bejing, China), pp. 14-23, IEEE Computer Society Press, September 2004. Available on-line from the CADP Web site in PDF or PostScript [vandePol-Espada-04-a] Jaco van de Pol and Miguel Valero Espada. "Modal Abstractions in mCRL". In Charles Rattray, Savitri Maharaj, and Carron Shankland, editors, Proceedings of the 10th International Conference on Algebraic Methodology and Software Technology AMAST'2004 (Stirling, Scotland, UK), Lecture Notes in Computer Science vol 3116, pp. 409-425, Springer Verlag, July 2004. [vandePol-Espada-04-b] Jaco van de Pol and Miguel Valero Espada. "An Abstract Interpretation Toolkit for mCRL". In Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems FMICS 2004 (Linz, Austria), Electronic Notes in Theoretical Computer Science, September 2004.
Contact:	Jaco van de Pol CWI, SEN 2 P.O. Box 94079 1090 GB Amsterdam THE NETHERLANDS Tel: +31 (0)20 592 4249 Fax: +31 (0)20 592 4199 E-mail: [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