This workshop, the first in a series of 5 organised by the FMERail project, was held at Breukelen, Netherlands on Monday 8 and Tuesday 9 June 1998. There were approximately 70 participants, with a good mix of railway experts and formal methods people, from both industry and academia. The format was that speakers were allowed 30 minutes each, followed by 15 minutes of questions and more general discussion. There were 6 presentations on Monday and 7 on Tuesday, and each day ended with a general discussion session. (One French speaker was unable to attend due to the French air pilots' strike.)

Before the first paper proper, participants were welcomed by Peter Gorm Larsen, on behalf of FMERail, who gave a plug for FME and the FM99 conference, and by Willy Enzing, on behalf of the local sponsors, Origin, who explained his company's interests in FM for the railway domain.

Max Geerling (Origin, NL): Modelling and Simulation: the LightRail perspective
LightRail is a system designed to be an intermediary between train and metro/tram, running as a tram in cities and as a train elsewhere. Modelling challenge is to investigate the effect the introduction of LightRail will have. What sort of traffic control procedures are needed, in the mixed-traffic situation (ie old trains/trams + LightRail). Origin has no experience in applying FM to this domain, but might be interested in projects if they are partially-funded, and can show expected benefit to Origin's activities.

Dines Bjorner (DTU, DK): The Railway Domain
Bjorner presented a RAISE specification of an `entire' railway system, comprising signalling, timetabling, shunting and marshalling. His view was that it was necessary to be able to describe a `whole' system, rather than just a small subsystem. Different interpretations of this specification could be given to various interested parties. The description used the axiomatic part of the RAISE language, with no explicit reference to the physical layout of the system. Interestingly, the description had been validated by explaining it to the 13 regions of Chinese railways: UNU staff had visited all of these regions. A long (121pp) report is in the proceedings.

Patrick Behm (Matra, France): Meteor: an industrial success in formal development
Behm described the experiences in using the B notation and tools to produce ATP software for the Meteor system (a new line for the Paris metro). It seems to have been a very successful use of FM, introducing a new notation to the company. The development produced c40,000 proof obligations. Initially only half of these were discharged by the automatic prover, but further customisation of the autoprover brought this up to 81%, and a further 11% were discharged via tactics and an improved rulebase. This left about 500 POs (mostly `mathematical' rules to be proved by hand, for c 100K lines of code. After development and proof effort, management decided not to use `the test line' as usual, but was happy to deploy immediately. In the year since that deployment, no errors have been found in the B-code, compared to an expectation of about 30 serious errors, based on the previous generation product. Estimate that proof effort cost about half of what functional test would cost. Overall costs were not increased.

Gea Kolk (Holland RailConsult, NL): A user's view of FM for railways
(Holland RailConsult was previously the research arm of Dutch Railways (NS) ) Kolk gave an overview of two different interlocking systems (VPI and EURIS) in use on Dutch Railways. The two subsequent talks gave more details. The overall prospects for FM in NS are positive.

Bas van Vlijmen (U.Utrecht, NL): VPI verification
The VPI system is intended for small stations: larger stations use EURIS. The system works on a 1 second cycle: read inputs, calculate, write outputs. The verification of VPI has been carried out using muCRL. Safety requirements are classified as STATIC (if phi holds now, the psi also holds now), NEXT (if phi holds now then n cycles ago, psi held), JUST (if phi holds now, then n cycles later, psi will hold).

Jan Friso Groote (CWI Amsterdam, NL): LARIS: a Language for Railway Interlocking Systems
The EURIS language (Middelraad 1982) has been used on Dutch Railways for some time. LARIS is intended to extend EURIS by removing certain restrictions. such as the fact that information only flows along tracks, and allowing infinite buffers between components.

Anne Haxthausen (DTU, DK): DRACOS: a distributed railway control system
A very elegant presentation of a RAISE specification of a simple network with trains at <= 100kph. No signals, but onboard computers and switch boxes at trackside. First an uncontrolled model is specified, then this is extended by 5 layers of algebraic spec, gradually becoming more explicit. State is not explicitly described until final layer, previously observer function give access to state information. Safety conditions described at each level: overall condition is their conjunction. Distinction is made between `safe' states and `consistent' states: the latter are closed under legal moves (so should these really be the `safe' ones??) Comments: Sterner: safety conditions are `wrong', since coupling/decoupling are not covered. When should we `turn off' safety requirements to allow transfer to `unsafe' states? Bjorner: it is useful to describe normal operation and shunting/marshalling separately. Woodcock: need to describe *whole* system to discuss safety. Ingleby: other safety aspects are not covered by model: flank protection, approach locking. These are part of UK interlocking, but are they generally used?? [V interesting discussion]

Paul Dechering (Hollandse Signaalapparaten, NL): Formalisation of SPLICE
SPLICE is an architecture for large-scale distributed embedded systems. The talk described a formal model for reasoning about architectures, based on Receptive Process Theory. Interesting idea, but no explicit connection to railway domain. Odd talk for this audience.

Mike Ingleby (Huddersfield Uni and BR Research, UK): A predicate logic for harmonised interlocking functions
Ingleby described a formalisation, in Prolog-like predicates, of the ERRI description of interlocking (see Godziejewski paper below). It's less abstract than the ERRI natural language, describing also geographic and communications context. Currently, can't disclose full formalisation, as it's property of BR Research, but hope to publish it later (by 9/98 workshop). No quantifiers in description; for political reasons. Comments: Woodcock: this is formalisation of a mechanism for safety, not a strategy. Bjorner: FM people need to teach railway people about the power of abstraction. Woodcock: what about structuring? A: decomposition method has been published, in terms of Galois connections.

Matthew Morley (Leeds Uni, UK): Semantics of Geographical Data Languages http://www.scs.leeds.ac.uk/mjm
Morley talked at length about why it is important to give a formal semantics to a GDL! Then briefly about the actual operational semantic description given.
Comments: Does it scale? A: typical GDL programs are v short, so this is not a problem. [Hmm: not sure this is true]

Arne Boralv (LoggikConsultt, Sweden): Prover Technology in Railways
Boralv described the use of NP-tools at ADTranz in Sweden for railway signalling systems. Safety properties are proved at two levels: first at object level, then at system level, using object level properties.

Bogdan Godziejewski (Euro Rail Research Institute, NL): Harmonisation of functional conditions of signalling systems
ERRI project A201 aims to produce informal specification of interlocking to enable European harmonisation. Common core specification, and also extensions and exceptions to be described. 21 interlocking functions described, 27 track elements. Transition diagram model used for interlocking functions, status word model used for track elements. Intention is to prepare FM description. Biggest variation is in additional safety rules in each country. Reports and documents can be bought from ERRI.

Markus Montigel (Alcatel, Austria): Formal model of dependencies in interlockings
Double vertex graph used to describe track topology. Aim is to avoid usual description of distant dependencies, HOW dangers are avoided; instead describe trains explicitly, WHAT are dangers, close dependencies.