Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Large Automatic Verification of a Control Program for a Railway Interlocking System
Speaker:Jakob Lyng Petersen
coming from:Department of Information Technology,Technical University of Denmark and Danish State Railways Consult
Speakers Bio:
Event Type:Talk
Visibility:D1, D2, D3, INET, D4, D5, RG1, MMCI, SWS
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Monday, 9 December 96
Duration:60 Minutes
Building:45 - FB14
In this talk, some results from a case study in automatic verification are

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.

Name(s):Martin Henz
Phone:(0681) 302-5625
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):