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 Sidorova, Proceedings
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.