|Final Report of the COST-247 Action|
Towards Mechanical Verification of Parts of the IEEE P1394 Serial Bus
Lars Kuehne (1), Jozef Hooman (2), Willem-Paul de Roever (1)
|(1) Christian-Albrechts-Universitaet zu Kiel|
|Institut fuer Informatik|
|Tel: +49 431 5604-74|
|Fax: +49 431 566143|
|E-mail: firstname.lastname@example.org , email@example.com|
|(2) Technical Applications Group|
|Computing Science Department|
|Eindhoven University of Technology|
|P.O. Box 513, NL-5600 MB Eindhoven|
|Tel: +31 - 40 - 2474283|
|Fax: +31 - 40 - 2468508|
The IEEE P1394 Serial Bus standard provides high performance connections for data transfer between hardware components and is especially well suited for connecting multimedia devices. To achieve its mechanical verification, a high level specification is developed for the asynchronous part of the P1394 Link layer, using the verification tool PVS. We derive a formal framework which closely resembles the state machine approach used in the standard document. In this framework, a new parallel combinator characterizes synchronous message passing between transitions for which a set of messages is exchanged atomically. The combinator is mechanically checked for being commutative and associative. As expected, unclarities, ambiguities and unforseen properties need to be resolved in the specification of the Link layer. To date, important Link Layer properties have been handproved using linear time temporal logic; the next aim of the authors is the mechanization of these proofs in PVS.
This presentation has been given during the COST-247 2nd International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia, June 18-19, 1997).
COST-247 Working Group(s):
This Page was prepared by Mark Jorgensen.