Solid State Interlocking (SSI), a computer-based railway signalling system, is used extensively by British Rail and also by other railway administrations. An interlocking is implemented as a generic program, the same for all areas, together with a geographic database which serves as a detailed map of the track and signalling equipment in a specific area of control. The authors formally model SSI behaviour as that of a finite state automaton with next-state and output functions defined by geographic data. Safety of interlocking is modelled as a family of predicates of state, and a proof strategy based on mathematical induction is designed for showing that safety predicates remain invariant over an indefinite number of cycles. The strategy allows for a mixed approach to proof: high-level and proof of lemmas relating to the transitivity of safety, and lower-level mechanized proof of detailed steps. The formal model also lends itself to investigation of the safety of behaviour patterns in the environment controlled by an interlocking. A pattern of is a subset of input sequences, and the automaton connects this to a set of states which remain invariant under such input. This connection is shown to induce topologies into state-space and into the environment.
Proving safety of a railway signalling system incorporating geographic data
Sicherheitserprobung eines Eisenbahnsigalsystems in Verbindug mit geograpischen Daten
1992
6 Seiten, 1 Bild, 8 Quellen
Aufsatz (Konferenz)
Englisch
Software Safety Technologies for Railway Signalling
British Library Online Contents | 1998
|Software safety technologies for railway signalling
IuD Bahn | 1999
|Railway signalling - achieving concurrent safety and reliability
British Library Conference Proceedings | 2001
|Safety critical computers for railway signalling applications
British Library Conference Proceedings | 1994
|Engineering Index Backfile | 1949
|