In this paper we present an approach for automated verification of train or from control systems which is based on model checking. The strategies and techniques applied are distinguished from comparable concepts of other authors in the following ways: (1) The control model to be verified is equivalent to executable machine code. As a con- sequence, there is no need for stepwise refinement and associated formal verification, in order to establish the conformance between the model and the executable software. (2) The well-known state explosion problems occurring frequently when checking complete railway control models are overcome by a combination of bounded model checking and inductive or compositional reasoning. (3) Since the verification approach is fully automated, it can be applied to each concrete control system, instantiated from a generic system using configuration data encoding the railway network and the routes to be controlled. This offers an alternative to more conventional (semi-formal) verification strategies, where the generic system is fully verified (so-called type certification), but only partial verification is exercised on the concrete instances.
Automated verification for train control systems
Automatische Verifikation von Steuerungs- und Regelungssystemen für Züge
2004
14 Seiten, 2 Bilder, 4 Tabellen, 18 Quellen
Conference paper
English
TRAIN VERIFICATION SYSTEM, TRAIN VERIFICATION METHOD AND GROUND DEVICE
European Patent Office | 2017
|Logic Verification of Collision Avoidance System in Train Control Systems
British Library Conference Proceedings | 2009
|Reliability verification of train control algorithm for Korean high-speed train
British Library Conference Proceedings | 2000
|