Authors:
 Phillip James (1), Yoshinao Isobe(2), Markus Roggenbach (1)

Affiliations:
  (1) Swansea University, UK
  (2) AIST, Tsukuba, Japan

Title: 
Verifying Train Control Software - An exercise in SAT-based Model Checking

Abstract:
In cooperation with the company Invensys, we verify interlockings of
real world train stations with respect to safety conditions.

Our modelling language is propositional logic: The initial
configuration of a train station is characterized by some
initialisation formula. The control program (in ladder logic, an ISO
standard) of the interlocking system is automatically translated into
a transition formula. The physical layout of the train station with an
abstract safety condition, e.g. `trains are separated by at least one
empty track segment', yields a concrete safety condition S.

Within system engineering it is vital not only to know if the system
is safe, but also what sequence of states leads to the
violation. Here, we apply two different techniques:

   Bounded model checking: Starting from the set of initial states, we
   compute the sets of states reachable in k system iterations. This
   yields either k-safety or an error trace to an unsafe state.

   Backwards reachability analysis: Starting from the set of states
   violating S, we compute the sets of states reachable in k backwards
   iterations of the system. Should this iteration stop the increase
   in the set of states without reaching an initial state, the system
   is safe; otherwise we output the error trace.

Experiments have demonstrated that our approach is feasable, when
using a SAT solver as the underlying verification tool.