Stop Press: workshop programme available in pdf form.

IEEE 1394 (FireWire) Workshop

International Workshop on Application of Formal Methods to IEEE 1394 Standard

Co-located with FME 2001 in Berlin, Germany
13th March 2001

Supported by
BCS Specialist Group Formal Aspects of Computing Science
Formal Methods Europe

Topic

Case studies have an important role to play at several stages in the development of a formal method. Comparative case studies, in which different formal methods are applied to the same specification problem, are especially illuminating because the similarities and differences between the methods are thrown into sharp relief. Such studies can also serve as benchmarks to be used in assessing new developments in formal methods. Previous comparative case studies include the steam boiler control problem, the the RPC memory case study, the robot production cell, the Light Control requirements engineering study, and the Invoicing Case Study.

The goal of this workshop is to create a comparative case study based around the protocols of the IEEE standard 1394 High Performance Serial Bus (reference IEEE 1394-1995 and the supplement IEEE 1394a-2000). The workshop will provide a forum for researchers and practitioners from industry and academia to discuss both completed work and work in progress related to formal specification, validation and verification of components of the IEEE 1394 High Performance Serial Bus.

The Problem

The IEEE 1394 High Performance Serial Bus (aka ``FireWire'') is a particularly useful source of case studies for several reasons. It is an international standard in communications with a clear, widely available statement of its definition. It is an important and ubiquitous component of modern multimedia systems so that there is widespread commercial interest in its correctness: companies such as Sun Microsystems, Apple, Philips, Microsoft, Sony and many others have been involved in its development. Finally, it is a complex system with a variety of aspects which pose a challenge to the capabilities of formal methods in both description and analysis.

The IEEE standard describes the bus in 3 layers (physical, link and transaction) and splits each layer into various phases, each of which encompasses a number of protocols. The main focus of the workshop will be the Tree Identify Protocol of the Bus Reset phase of the physical layer. Participants are encouraged to consider the problems of formalising and analysing this protocol. More details about this protocol are available here. In addition, we have obtained permission to reprint those sections of the IEEE standard and supplement directly related to the Tree Identify Protocol.

The workshop is not restricted to the Tree Identify Protocol as there are many other components of the 1394 standard which are also amenable to formal description and analysis. For example, parts of the link layer have been formally specified. Also, there are ongoing standardisation development projects based around the 1394. For example, P1394b (a faster version of 1394), P1394.1 (bus bridges), and P1394.3 (peer to peer data transport protocol). Formal descriptions of any aspect of the 1394 standard and associated developments may be submitted for inclusion in the workshop.

You may find it helpful to consult the full standard 1394-1995 as well as the supplement 1394a-2000 (IEEE standards site).

The Workshop

The workshop will be co-located with FORMAL METHODS EUROPE 2001 "Formal Methods for Increasing Software Productivity" 12-16 March 2001, Humboldt-Universitaet zu Berlin, Germany.

The workshop will be held on 13th March.

Submission

You are invited to submit a 2-4 page abstract on formalising and analysing some aspect of the IEEE 1394 Standard. Preference will be given to those works detailing some analysis of the system as well as a formal description. We invite both completed work and work in progress; the aim of the workshop is to stimulate discussion.

In the spirit of Abrial's Steam Boiler Case Study we are posing some questions which are intended to facilitate comparison of the different methods. See further details. The abstract need not contain full answers to these questions, but the full paper submission must.

Submission should be made electronically to firewire-workshop@cs.stir.ac.uk. We accept plain text, pdf or postscript submissions.

Authors of accepted abstracts will be expected to give a 20 minute presentation at the workshop.

Important Dates

19th January 2001 Submission of abstracts
2nd February 2001 Notification of Acceptance
9th February 2001 Early registration deadline for FME
13 March 2001 Workshop
15th June 2001 Submission of full papers
Note: workshop participants must register for FME 2001 to attend the workshop. There is a special one day registration fee available.

Workshop Committee

Carron Shankland,
Savi Maharaj,
Department of Computing Science and Mathematics, University of Stirling.

Judi Romijn,
Computing Science Department, University of Nijmegen.

Publication

The accepted abstracts will be published as a University of Stirling Technical Report which will be available at the workshop. Authors of selected papers will be invited to submit full (and revised) papers for a special issue of 'Formal Aspects of Computing' after presentation at the workshop.

Last revision: 8th March 2001.