Special Issue of FACS on Application of Formal Methods to IEEE 1394 Standard

Call for Full Papers

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

Following a successful workshop in Berlin on this topic, we are calling for full papers for a special issue of 'Formal Aspects of Computing'. Jump to submission details.

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.

Our goal 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 provided 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. Now we're calling for papers for a special issue of Formal Aspects of Computing Science. The call is mainly addressed to those who presented an abstract at the workshop, but is also open to others.

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. Contact us with your postal address for a copy.

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. We have negotiated a special arrangement with IEEE for bulk ordering at substantially reduced cost (half normal non IEEE member price). Contact us to find out more. You may also wish to visit the IEEE standards site.

The Workshop

The workshop programme is available, together with links to presented abstracts. Those intending to submit who did not attend the workshop should make themselves familiar with the papers presented at the workshop.

Submission

You are invited to submit a full paper 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. The document should adhere to the style requirements of 'Formal Aspects of Computing'. For your convenience, you can download the appropriate LaTeX style files and guides: fac.cls, fac.sty, cls_guide.tex, style_guide.tex,

Maximum page length (in this style) is 12 pages.

Note: most of the workshop papers were concerned with some aspect of the Tree Identify Protocol, therefore, we will supply an introductory paper describing the 1394 Standard in general, and the Tree Identify Protocol in particular. You should not give a general description of these things in your own paper. Download a draft of the introductory paper. If you feel there is something missing, let us know.

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

Comparison of the Approaches

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 paper should not necessarily contain answers to these questions; please submit the answers to us separately by email to facilitate writing of the introductory paper.

Important Dates

Deadline for submission of full papers is 31st July 2001.

Workshop Committee

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

Judi Romijn,
Computing Science Department, University of Nijmegen.


Last revision: 3rd May 2001.