Automatically Verifying Railway Interlockings using SAT-based Model Checking
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:
PDFDOI: 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.