New directions in Symbolic Model Checkning for Real-Time Systems

Project no: 9811-6

Parosh Abdulla

Uppsala University, Informationtechnology

Application as pdf, ps Complement to application as ps, pdf, support letter 1 from Banverket and support letter 2 from Prover Technology AB

Support: 1 PhD student for 2 years decided 98-12-09.

Start 99-08-01 with Julien D'Orso as Phd student.

Reports: 1-year-report 00-08-22

Local web: http://www.docs.uu.se/~parosh/projects/smc/

 

Industry contacts

Gunnar Stålmarck gunnar@prover.com

Prover Technology AB

Stockholm

Project: New directions in Symbolic Model Checkning for Real-Time Systems

Overview

Real-time embedded systems are increasingly becoming parts of our everyday life. Examples range from TV's and telephone switches to safety-critical systems such as railway control, air traffic control, and patient monitoring systems. The behaviour of such a system is typically ``reactive'' in the sense that it reacts to interactions with a physical environment. It is widely recognized that it is extremely difficult to produce error-free implementations of reactive systems. Although the software industry is moving towards a more systematic approach to design, extensive simulation is still common practice to ensure the conformance of a system implementation with its intended specification. However, the complexity of the system in hand makes it usually infeasible to guarantee correctness through the use of simulation. It is therefore important to complement simulation with systematic validation and verification. This allows early detection of flaws, thus reducing the life cycle cost of the system. In fact it is acknowledged by designers that errors can often be traced back to mistakes which should be possible to discover at a much earlier stage of the design process. This project intends to unify several existing techniques and invent new ones for verification of real-time systems.

We plan to develope techniques suitable for the verification of Programmable Logic Controllers (PLCs). PLCs is one of the most important platforms for the realization of programmed control. They provide a uniform hardware solution which can be flexibly programmed in software. Formal verification techniques have achieved some notable success for verification of PLC-based control software in railway signalling systems The technology has the potential to shorten development times for control software by an order of magnitude. The aim of the current project is to further develop this approach.

Results

We have implemented a prototype for symbolic model checking based on Stålmarck's algorithm (instead of BDDs). We have obtained permission from prover to use their tool in our implementation. We have regular common progress meetings (once a month).

Early results are very promising. A research report has been submitted to the "International Conference on Tools and Algorithms for the Construction and Analysis of Systems".

Co-operation

Cooperation within Sweden

We cooperate with the ASTEC project "New Directions in Symbolic Model Checking" and with the group of Mary Sheeran at Chalmers.

Publications

1. Parosh Aziz Abdulla, Per Bjesse, and Niklas Eén. Symbolic Reachability Analysis Based on SAT-Solvers. To appear in Proc. TACAS'2000, 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems.