AUTOMATED VERIFICATION FOR TRAIN CONTROL SYSTEMS
Author: Jan Peleska, Daniel Große, Anne E. Haxthausen and Rolf Drechsler
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.