CWI and the Eindhoven University of Technology (THE NETHERLANDS)
muCRL (micro Common Representation Language)
CADP (Construction and Analysis of Distributed Processes)
Certain communication protocols, such as the PAR (Positive
Acknowledgement Retransmission) protocol, depend essentially upon
the values of timeouts, and therefore behave as timed rather than
untimed systems. The objective of this work is to establish a framework
for verifying timed systems using the techniques and tools available
for untimed systems. The approach consists in extending the muCRL
specification language with a special action tick, which models
one unit of time elapsing. This allows to use the muCRL toolset in
order to produce the state space of a timed system, which is
subsequently analyzed using the CADP verification toolbox.
The PAR protocol consists of a sender, a receiver, and two unreliable communication channels for messages and acknowledgements. A new message is sent only when the preceding one has been acknowledged. The sender detects the loss of a message (or acknowledgement) by using a timeout. In order to avoid erroneous behaviours of the PAR protocol, such as the undetection of a message loss, the timeout interval must be larger than the sum of transmission delays on the message and acknowledgement channels, and delivery delay taken by the receiver. Starting from a specification of the PAR protocol in which delays are represented using timers, the corresponding state space was generated using the muCRL toolset. Several (untimed) safety and liveness properties were specified in regular alternation-free mu-calculus and successfully verified on the state space with the EVALUATOR model-checker of CADP.
In order to express properties involving quantitative time, a timed, action-based variant of LTL (Linear Temporal Logic), called path-restricted LTL, was defined. This logic can be translated into (untimed) modal mu-calculus by encoding time constraints using tick actions. The resulting mu-calculus formulas can be verified on the state space by using the EVALUATOR model-checker of CADP.
This study demonstrated that classical (untimed) process algebraic
languages allow to describe timed systems by an appropriate
introduction of special discrete actions representing the passage
of time. The resulting descriptions can be analyzed by using tools
originally dedicated to untimed systems, such as muCRL and CADP.
Stefan Blom, Natalia Ioustinova, and Natalia Sidorova.
"Timed Verification with muCRL". 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 our FTP site in PDF or PostScript
Dr. Stefan Blom
CWI / Department of Software Engineering
SEN2 (Specification and Analysis of Embedded Systems)
Kruislaan 413, 1098 SJ Amsterdam, The Netherlands
Tel: +31 20 592 4099
Fax: +31 20 592 4199
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|