- New directions in Symbolic Model Checkning for Real-Time
- Project no: 9811-6
- Parosh Abdulla
- Uppsala University, Informationtechnology
- Application as
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/
- Gunnar Stålmarck email@example.com
- Prover Technology AB
- Project: New directions in Symbolic Model Checkning for Real-Time Systems
Real-time embedded systems are increasingly becoming parts of our
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
Although the software industry is moving towards a more systematic approach to design,
is still common practice to ensure the conformance of a system implementation with its
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
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
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".
Cooperation within Sweden
We cooperate with the ASTEC project "New Directions in Symbolic
Model Checking" and with the group of Mary Sheeran at Chalmers.
- 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.