Automatic Verification of the IEEE 1394 Tree Identify Protocol

Organisation:	University of Tehran and IPM (IRAN) Eindhoven University of Technology TU/e (THE NETHERLANDS) Reykjavík University (ICELAND)
Method:	Rebeca mCRL2 μ-calculus
Tools used:	mCRL2 tool-set Sarir CADP (Construction and Analysis of Distributed Processes)
Domain:	Communication Protocols.
Period:	2007
Size:	n/a
Description:	This paper addresses the verification of actor-based programs written in the reactive object language Rebeca, which has a formal foundation and is designed in an effort to bridge the gap between formal verification approaches and real applications. A Rebeca model contains concurrent objects (called rebecs) that modify their local state and send asynchronous messages in reaction to received messages. Rebecs dequeue received messages from infinite queues and execute the corresponding methods atomically (i.e., without interleaving statements of concurrent methods). When several rebecs can dequeue a message, a nondeterministic scheduler chooses the message to dequeue. The verification approach consists in translating Rebeca models into the mCRL2 process algebra. Atomicity of message execution allows to replace concurrent behavior by nondeterministic sequential interleaving; moreover, at any time, only one instance from the rebecs and the scheduler processes needs to be present (in addition to a process for the state variables of the rebecs and one for their queues). This translation is automated by a tool, called Sarir. Then, the state space is generated as a labeled transition system (LTS), where transitions correspond to message sending and to assignment to local state of rebecs. In a third step, various reductions and minimizations can be applied to the LTS and properties are checked against the LTS using the EVALUATOR tool of CADP. The approach is illustrated on four examples among which the tree identify phase of the IEEE 1394 firewire bus. When a component is removed or attached to a firewire bus, the resulting topology is checked to be a tree or not. To determine the root of the tree, nodes exchange parent request messages. The property checked with the EVALUATOR tool verifies that the root is always correctly determined.
Conclusions:	This work illustrates the usefulness of the model checking approach with CADP of actor-based programs. Despite conceptual differences between source and target models, the tool chain proved to be effective for the purpose of verification: "The results are encouraging and show significant improvement (esp. in large case-studies) over an existing translation into Promela, the input language of the Spin model-checker."
Publications:	[Hojjat-Sirjani-Mousavi-Groote-07] H. Hojjat, M. Sirjani, M. R. Mousavi and J. F. Groote. "Sarir: A Rebeca to mCRL2 Translator". In Proceedings of the 7th International Conference on Application of Concurrency to System Design ACSD'07 (Bratislava, Slovak Republic), pp. 216-222, IEEE Computer Society, July 2007 Available on-line from http://www.win.tue.nl/~mousavi/acsd07.htm or from the CADP Web site in PDF or PostScript
Contact:	Marjan Sirjani School of Electrical and Computer Engineering University of Tehran Karegar Avenue, Pardiss 2 Tehran, Iran Tel: + 98 21 6111 4912 E-mail: msirjani@ut.ac.ir http://ece.ut.ac.ir/msirjani
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