Automatically Verifying Railway Interlockings using SAT-based Model Checking

Phillip James, Markus Roggenbach

Abstract


In this paper, we demonstrate the successful application of various SAT-based model checking techniques to verify train control systems. Starting with a propositional model for a control system, we show how execution of the system can be modelled via a finite automaton. We give algorithms to perform SAT-based model checking over such an automaton. In order to tackle state-space explosion we propose slicing. Finally we comment on results obtained by applying these methods to verify two real-world railway interlocking systems.

Full Text:

PDF


DOI: http://dx.doi.org/10.14279/tuj.eceasst.35.547

DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.35.547.585

Hosted By Universit├Ątsbibliothek TU Berlin.