Verification of interlocking systems using statistical model checking

TL;DR

This paper introduces a statistical model checking approach for verifying interlocking systems in railway stations, balancing scalability and confidence in safety and availability properties.

Contribution

It presents a novel verification method combining model checking and simulation to assess large interlocking systems with quantifiable confidence.

Findings

Enables verification of larger stations than traditional model checking

Provides probabilistic guarantees on safety and availability properties

Balances scalability and verification confidence

Abstract

In the railway domain, an interlocking is the system ensuring safe train traffic inside a station by controlling its active elements such as the signals or points. Modern interlockings are configured using particular data, called application data, reflecting the track layout and defining the actions that the interlocking can take. The safety of the train traffic relies thereby on application data correctness, errors inside them can cause safety issues such as derailments or collisions. Given the high level of safety required by such a system, its verification is a critical concern. In addition to the safety, an interlocking must also ensure that availability properties, stating that no train would be stopped forever in a station, are satisfied. Most of the research dealing with this verification relies on model checking. However, due to the state space explosion problem, this approach does not scale for large stations. More recently, a discrete event simulation approach limiting the verification to a set of likely scenarios, was proposed. The simulation enables the verification of larger stations, but with no proof that all the interesting scenarios are covered by the simulation. In this paper, we apply an intermediate statistical model checking approach, offering both the advantages of model checking and simulation. Even if exhaustiveness is not obtained, statistical model checking evaluates with a parametrizable confidence the reliability and the availability of the entire system.