Formal Verification of relay-based interlocking systems at MTA NYCT

In a project for MTA New York City Transit, the objectives were to

• Define an informal specification, in natural language, of the safety requirements that all NYCT interlocking systems shall satisfy.

• Define a formal, mathematically exact specification of the generic safety requirements for NYCT’s interlocking systems, in the Prover iLock specification language PiSPEC.

• Formally verify the Chambers St interlocking system, which was updated concurrently, against the generic safety requirement specification using Prover iLock.

Safety requirements

A major part of this project was to capture the safety requirements that NYCT interlocking systems shall satisfy. Prover Technology collaborated with experts in NYCT signaling systems in the process of defining the safety requirements. The safety principles were defined generically, to be applicable in principle to any NYCT interlocking configuration of switches and signals. The resulting specification consisted of two parts:

• A non-formal specification of safety requirements in natural language, including a description of relevant design principles of relay-based interlocking systems for NYCT.

• A formal specification of safety requirements in PiSPEC. This specification can be configured and automatically instantiated by Prover iLock for specific interlocking systems.

The safety requirement specification developed defines twenty-seven generic safety requirements in total.

Interlocking system implementation

The Chambers St interlocking system was implemented using vital relays, conforming to NYCT signaling principles standards. The standards are defined as relay schematics that describe circuit design solutions that meet both operational requirements (to provide operational functionality) and safety requirements (to ensure safe operation and preventing accidents).

While vital relays are exceptionally reliable and long-lived hardware components, they inevitably fail at some point. The safety of a signaling system should not be compromised by the failure of a single component, since such failures are likely to occur from time to time. A particularly complex aspect of the design and review process is to grasp the safety implications of component failures. With systems consisting of hundreds (or in some cases thousands) of vital relays, it is non-trivial to perform validation and verification of such systems.

In order to analyze the behavior of a relay-based interlocking system an accurate and complete model of the entire design circuit needs to be established. This includes modeling each (relay) component, power sources, current-conducting elements (such as cables and wires) and so on. The verification model of the Chambers St interlocking system was created by converting the circuit schematics database (on Microstation DGN format) using Prover Extractor.

Safety verification

The Chambers St interlocking system was analyzed with respect to the safety requirements in two steps:

• The nominal analysis proved all safety requirements under the assumption that all relay components function correctly (no failures)

• The failure mode analysis proved all safety requirements under the assumption that one relay component is failing.

The nominal analysis revealed flaws originating from mistakes in the relay circuit design process. The failure mode analysis, on the other hand, revealed situations that led to updates to the established signaling principles underlying NYCT relay circuit designs.