Supported by BCS Specialist Group Formal Aspects of Computing Science Formal Methods Europe
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 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 will be held on 13th March.
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 firstname.lastname@example.org. We accept plain text, pdf or postscript submissions.
Authors of accepted abstracts will be expected to give a 20 minute presentation at the workshop.
|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|
Computing Science Department, University of Nijmegen.