Automatic Verification of the IEEE 1394 Root Contention Protocol.

Organisation:	University of Twente (THE NETHERLANDS) and University of Birmingham (UNITED KINGDOM)
Method:	Probabilistic Timed Automata Probabilistic Labelled Transition Systems Markov Decision Processes
Tools used:	CADP (Construction and Analysis of Distributed Processes) KRONOS PRISM
Domain:	Communication Protocols.
Period:	2002-2004
Size:	n/a
Description:	Real-time aspects of communication protocols that perform in the presence of lossy media, are frequently specified using soft deadlines, such as "with a probability of at least 0.96, video frames arrive within 80 to 100ms after being sent". The objective of this work is to show how classical (non-probabilistic) tools can be combined with probabilistic tools for the automatic verification of the root contention protocol of IEEE 1394, a timed and probabilistic protocol to resolve conflicts between two nodes competing in a leader election process. The property of interest is the minimal probability that a leader has been elected before a given deadline. The starting point of the verification is a classical timed automata model of the protocol. After extending this model with probabilities, KRONOS is used to generate the corresponding forward reachability graph, which is reduced with respect to probabilistic bisimulation using the BCG_MIN tool of CADP. The minimized graph is finally transformed into a Markov Decision Process which is used to verify the desired properties using the model checker PRISM.
Conclusions:	This study demonstrated that minimization with respect to probabilistic bisimulation using CADP, which reduces the state space by more than an order of magnitude, is a useful preprocessing step for probabilistic model-checkers, enabling the verification of large examples.
Publications:	[Daws-Kwiatkowska-Norman-02] Conrado Daws, Marta Z. Kwiatkowska, and Gethin Norman. "Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM". In Proceedings of the 7th International Workshop on Formal Methods for Industrial Critical Systems FMICS'02 (Malaga, Spain), Electronic Notes in Theoretical Computer Science vol. 66(2), 2002. Available on-line at: http://www.cs.bham.ac.uk/~dxp/publications/DKN02.html or from the CADP Web site in PDF or PostScript [Daws-Kwiatkowska-Norman-04] Conrado Daws, Marta Z. Kwiatkowska, and Gethin Norman. "Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM". International Journal on Software Tools for Technology Transfer (STTT), Volume 5(2-3), pp. 221-236, March 2004. Available on-line at: http://www.cs.bham.ac.uk/~dxp/publications/DKN04.html or from the CADP Web site in PDF or PostScript
Contact:	Dr. Conrado Daws Faculty of Science, University of Nijmegen Postbus 9010, 6500 GL Nijmegen THE NETHERLANDS Tel: +31 24 3652590 E-mail: C.Daws@cs.ru.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