Large Automatic Verification of a Control Program for a Railway Interlocking System

The ultimate goal of the case study is to prove all safety requirements of a
control program for an interlocking system in use at a fairly sized Swedish
rail yard.

The semantics of the control program, written in the special-purpose language
STERNOL, can be translated into propositional logic. The resulting formula then
describes the relation between all possible inputs and outputs to/from the
program. Since the safety requirements can also be expressed in propositional
logic, the problem of verifying that all requirements are fulfilled by the
program is a decidable problem. However, since the potential state space of the
program is very large ($> 10^{10^{5}}$) in practice, most decision procedures
cannot be directly applied.

In this case study, a theorem prover based on the St{\aa}lmarck algorithm was
applied to the problem. The algorithm is based on the concept of {\em degree
of hardness} of proofs. The St{\aa}lmarck algorithm can do proofs in
polynomial time, where the degree of the polynomial is proportional to the
degree of hardness of the proof. A main point of applying the St{\aa}lmarck
algorithm is, that in practice, proving properties of industrial systems
is often of a low degree of hardness, thereby making it feasible to prove
requirements for fairly sized systems.

Problems occur if the degree of the proofs are high or if the prover has to
find a counter example. We then have to find ways to reduce the
system. An idea of ``projecting'' the system with respect to a given
requirement is presented.

By projecting the system with respect to requirements, very large reductions
(typically around 75% of the system) are obtained. The effect of
the reduction is, that is becomes feasible to search for proofs of a higher
degree of hardness which would have been infeasible before the system was
projected. Also, it becomes feasible to find counter models for subsystems.