OUCL,
Wolfson Building,
Parks Road,
Oxford OX1 3QD,
United Kingdom
The first FMERail workshop was held in Breukelen, Netherlands, on the 8th and 9th of June 1998. It attracted many participants, both from academia and industry. There were 13 presentations, each of which lasted 30 minutes, with a further 15 minutes being allocated for questions. In addition, there was plenty of time available for discussions of a more general nature.
The contributions of each of the speakers are summarised below.
Modelling and Simulation for Innovative Train Protection and Control: The Light Rail Perspective Max Geerling, Origin
Geerling reported on work carried out by Origin in the Netherlands. LightRail is a system which is designed to be an intermediary between trains and trams: it runs as a tram in cities and as a train elsewhere. One of the challenges of modelling in this context is to investigate how the introduction of LightRail will have on existing systems; e.g., what sort of traffic control procedures are required when existing trams and trains interact with LightRail? Information about this work is available at http://www.origin-it.co.
Bjorner reported on joint work carried out with Chris George, Bo Stig Hansen, Hans Laudrup and Soren Prehn at the Technical University of Denmark. A formal specification in RAISE [RAISE 1992, RAISE 1995] of a railway system was described, including such diverse features as signalling, timetabling, shunting and marshalling: the authors feel that it is necessary to be able to describe a system as a whole, rather than as a series of smaller subsystems. The description used the axiomatic part of the RAISE language, with no explicit reference to the physical layout of the system. The work is described in a technical report [Bjorner et al 1997].
Behm reported on joint work carried out with Jean-Marc Meynadier at Matra in France. Behm described a successful use of formal methods: the application of the B notation and tools to produce Automatic Train Protection (ATP) software for the Meteor system in Paris. The development resulted in approximately 40,000 proof obligations; no errors have been found in the code since deployment.
Kolk reported on work carried out at Holland Railconsult. An overview of two different interlocking systems - Vital Processor Interlocking (VPI) and EUropean Railway Interlocking Specification (EURIS) - was presented. This presentation, which was based on [Kolk 1998], set the scene for the next two talks.
van Vlijmen reported on work carried out at the University of Utrecht. The VPI system, which is intended for small stations, works on a one second cycle: read inputs, calculate, write outputs. The verification of VPI has been carried out using mu-CRL[Groote and Ponse 1994, Groote and Ponse 1995], and is described further in [Groote et al 1994] and [Groote et al 1995].
Groote reported on work carried out with Marco Hollenberg and van Vlijmen at CWI and the University of Utrecht. The EURIS language [Berger et al 1992] has been used on Dutch Railways for some time. LARIS, the language described in this talk, is intended to extend EURIS by removing certain restrictions, e.g., the fact that information only flows along tracks.
Dechering reported on work carried out with Rix Groenboom, Edwin de Jong, and Jan Tijmen Udding at Hollandse Signaal Apparaten and the University of Groningen. SPLICE is an architecture for large-scale distributed embedded systems. The presentation described a formal model for reasoning about architectures, which is based on Receptive Process Theory.
Haxthausen reported on work carried out with Jan Peleska at the Technical University of Denmark and the University of Bremen. A RAISE specification of a simple network was presented. A distinction is made between safe states and consistent states: those which are closed under legal moves.
Ingleby reported on work carried out at the University of Huddersfield. A formalisation of an interlocking was described in terms of Prolog-like predicates. The model is less abstract than the ERRI natural language description: it describes both geographic and communications contexts.
Morley reported on work carried out at the University of Leeds. It was argued that it is important to give a formal semantics to geographic data languages. An example of an operational semantics was provided.
Boralv reported on work carried out with Gunnar Stalmarck at Prover Technology in Sweden. The use of NP-tools at ADTranz in Sweden was described. Safety properties are proved at two levels: first at the object level, then at the system level, using object level properties. The presentation was based on [Boralv and Stalmarck 1998].
Godziejewski reported on work carried out with Y. Hirao at the European Rail Research Institute and the Railway Technical Research Institute. ERRI project A201 aims to produce informal specification of interlocking to enable European harmonisation: it describes 21 interlocking functions and 27 track components. Transition diagram models are used for interlocking functions and status word models are used for track elements: the intention is to prepare a formal description.
Montigel reported on work carried out at Alcatel in Austria. Double vertex graphs are used to describe track topology. The overall aim of the work is to avoid the usual descriptions of distant dependencies.
The variety of presentations and participants meant that discussions were meaningful and threw up many open research questions.
I, as I am sure many others do, look forward to future events in this series.
[Berger et al 1992]
J. Berger, P. Middelraad, and A. J. Smith.
EURIS, European Railway Interlocking Specification, May 1992.
[Boralv and Stalmarck 1998]
A. Boralv and G. Stalmarck.
Prover technology in railways.
In M. G. Hinchey and J. P. Bowen, editors,
Industrial-Strength Formal Methods. Academic Press, 1998.
[Groote et al 1994]
J. F. Groote, J. W. C. Koorn, and S. F. M. van Vlijmen.
The safety guaranteeing system at station Hoorn-Kersenboogerd.
Technical Report 121, Utrecht University, Logic Group Preprint Series
of the Department of Philosophy, 1994.
[Groote et al 1995]
J. F. Groote, J. W. C. Koorn, and S. F. M. van Vlijmen.
The safety guaranteeing system at station Hoorn-Kersenboogerd.
In Proceedings of the Tenth Annual Conference on Computer Assurance,
Compass '95, pages 57-68. IEEE, 1995.
[Groote and Ponse 1994]
J. F. Groote and A. Ponse.
Proof theory for mu-CRL: a language for processes with data.
In D. J. Andrews, J. F. Groote, and C. A. Middelburg, editors,
Proceedings of the International Workshop on Semantics of Specification
Languages, pages 232-251. Springer-Verlag, 1994.
[Groote and Ponse 1995]
J. F. Groote and A. Ponse.
Syntax and semantics of mu-CRL.
In A. Ponse, C. Verhoef, and S. F. M. van Vlijmen, editors,
Algebra of Communicating Processes, Utrecht, 1994, pages 26-62.
Springer-Verlag, 1995.
[Kolk 1998]
G. Kolk.
Formal methods: Possibilities and difficulties in a railway environment from
a user perspective.
In Proceedings of the Third International Workshop on Formal
Methods for Industrial Critical Systems, May 25-26, 1998, 1998.
[RAISE 1992]
The RAISE Specification Language.
The BCS Practitioners Series. Prentice-Hall International, 1992.
[RAISE 1995]
The RAISE Development Method.
The BCS Practitioners Series. Prentice-Hall International, 1995.