Verification of railway interlocking - Compositional approach with OCRA

TL;DR

This paper presents a compositional verification approach for railway interlocking systems using the OCRA tool, enabling scalable safety verification of complex station models with advanced algorithms.

Contribution

It introduces a method combining OCRA modeling with compositional verification and new algorithms in NuSMV for verifying safety properties of railway interlockings.

Findings

Successful modeling of a medium-sized station with OCRA

Verification of safety properties using contracts and compositional methods

Application of k-liveness and IC3 algorithms for LTL property verification

Abstract

In the railway domain, an electronic interlocking is a computerised system that controls the railway signalling components (e.g. switches or signals) in order to allow a safe operation of the train traffic. Interlockings are controlled by a software logic that relies on a generic software and a set of application data particular to the station under control. The verification of the application data is time consuming and error prone as it is mostly performed by human testers. In the first stage of our research, we built a model of a small Belgian railway station and we performed the verification of the application data with the nusmv model checker. However, the verification of larger stations fails due to the state space explosion problem. The intuition is that large stations can be split into smaller components that can be verified separately. This concept is known as compositional verification. This article explains how we used the ocra tool in order to model a medium size station and how we verified safety properties by mean of contracts. We also took advantage of new algorithms (k-liveness and ic3) recently implemented in nuxmv in order to verify LTL properties on our model.