Positive Acknowledgement Retransmission (PAR) Protocol.

Organisation:	CWI and the Eindhoven University of Technology (THE NETHERLANDS)
Method:	muCRL (micro Common Representation Language)
Tools used:	muCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Communication Protocols.
Period:	2003
Size:	n/a
Description:	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.
Conclusions:	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.
Publications:	[Blom-Ioustinova-Sidorova-03] 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 the CADP Web site in PDF or PostScript
Contact:	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 E-mail: Stefan.Blom@cwi.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page