CWI (Amsterdam, THE NETHERLANDS)
Abstract Model Checking
CADP (Construction and Analysis of Distributed Processes)
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.
The Abstract Interpretation Toolkit for mCRL and EVALUATOR have been
successfully experimented in several case studies, such as JavaSpaces
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 our FTP 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.
Jaco van de Pol
CWI, SEN 2
P.O. Box 94079
1090 GB Amsterdam
Tel: +31 (0)20 592 4249
Fax: +31 (0)20 592 4199
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|