next up previous

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
Preusserstr. 1-9
D-24105 Kiel
Tel: +49 431 5604-74
Fax: +49 431 566143
E-mail: ,
(2) Technical Applications Group
Computing Science Department
Eindhoven University of Technology
P.O. Box 513, NL-5600 MB Eindhoven
The Netherlands
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):

Web Links : , ,

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page