CWI (Amsterdam, THE NETHERLANDS)
Connection of the mCRL toolset to OPEN/CAESAR
MCRL.OPEN is a new tool that allows to apply the on-the-fly
verification tools of CADP (OPEN/CAESAR) to descriptions written
using the mCRL process algebra, developed at CWI Amsterdam.
MCRL.OPEN takes as inputs an OPEN/CAESAR verification tool with appropriate arguments and a mCRL description, which has been first transformed into an intermediate (so-called linearized) form using the mCRL toolset.
MCRL.OPEN translates the linearized mCRL description into its corresponding transition system, represented implicitly (i.e., by means of its successor function) according to the OPEN/CAESAR generic API. It then executes the OPEN/CAESAR verification tool on this implicit representation.
MCRL.OPEN was developed in the framework of the SENVA collaboration
between the VASY team of INRIA and the SEN2 group of CWI. It is
available as a component of the mCRL toolset.
|Publications:||The SENVA 2004 Activity Report http://vasy.inria.fr/senva/report2004.html|
Jaco van de Pol
P.O. Box 94079
1090 GB Amsterdam
Tel: +31 (0)20 592 4137
Fax: +31 (0)20 592 4199
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|