Natalia Ioustinova , Specification and Analysis of Embedded Systems

Timed Verification with mCRL


mCRL, CADP

µCRL (micro CRL - written as mCRL if the symbol µ is not available) is a process algebraic language that was especially developed to take account of data in the study of communicating processes. µCRL is supported by a collection of tools, the µCRL toolset. The µCRL toolset currently comprises a well-formedness checker, a linearizer, a simulator, a state space generator as well as a few tools to analyze and optimize LPOs. The generated state space can be read, visualized and manipulated by VASY's Cæsar/Aldébaran Development Package (CADP). For more information about  µCRL and CADP, please, visit the corresponding web-pages.



Timed verification with mCRL

µCRL  powerful formalisms that is able to handle both data and behaviour aspects of reactive systems but  originally is not aimed at the verification of time issues. Here we provide a framework that allows to use the existing untimed language and the toolset for timed verification without introducing any syntactical or semantical changes into the language, and without modifying the toolset.

We restricted ourselves to the relative discrete time. Time progression is modelled as a tick-action  that represents elapsing one unit of time. A timed parallel composition operator is defined in terms of basic  µCRL operators. Time progression has the least priority
in the system. This property, called maximal progress, is usually expressed by introducing priority operators. We avoid the introduction of new operators providing a special specification discipline that allows us to stay within µCRL syntax and semantics.

The proposed discrete-time semantics is suitable to express time aspects and analyse time properties of a large class of reactive systems.  We justified the usefulness of  our approach by the verification experiments on \mCRL\ specifications of the positive
acknowledgment retransmission protocol (PAR) and the bounded retransmission protocol (BRP) whose behaviour depends  on the timers' settings.

To express not only qualitative but also quantitative timed properties of systems, we introduced an  LTL-like action-based timed temporal logic and showed how to encode its time constraints with the use of  "tick", which results untimed temporal formulas. These formulas can then be translated to the regular alternation free µ-calculus and checked with the CADP toolset. The LTL-like action-based timed temporal logic together with the specification discipline provide the framework for the timed verification with untimed  µCRL and CADP toolsets.

Timed verification with mCRL, Stefan Blom, Natalia Ioustinova, and Natalia SidorovaProceedings of the 5th Andrei Ershov International Conference on Perspectives of System Informatics PSI'2003 (Novosibirsk, Russia), Lecture Notes in Computer Science vol. 2890, pp. 178-192, July 2003.  Available on-line at: http://www.cwi.nl/ftp/CWIreports/SEN/SEN-E0312.pdf
or from the VASY FTP site in PDF or PostScript


Test Examples

BRP: brp.tar.gz.
PAR: par.tar.gz.

To try them decompress the archive with

gzip -d mCRLbrp.tar.gz


If you have any problems with the archives, or want some more information, please write to Nataliya Yustinova: ustin@cwi.nl.