AUTOMATED VERIFICATION FOR TRAIN CONTROL SYSTEMS

Author: Jan Peleska, Daniel Große, Anne E. Haxthausen and Rolf Drechsler

Abstract:
In this paper we present an approach for automated verification of train or tram 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 consequence, 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.

postscript file (114KB)