max planck institut
informatik

# 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)
Title: Large Automatic Verification of a Control Program for a Railway Interlocking System Jakob Lyng Petersen Department of Information Technology,Technical University of Denmark and Danish State Railways Consult Talk D1, D2, D3, INET, D4, D5, RG1, MMCI, SWSWe use this to send out email in the morning. AG Audience English
Date: Monday, 9 December 96 14:15 60 Minutes Saarbrücken 45 - FB14 528
 In this talk, some results from a case study in automatic verification are presented. 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 (0681) 302-5625 --email address not disclosed on the web