Symbolic Model Checking

Presentation

Symbolic Model Checking showed to be an effective method to handle large and potentially infinite state systems. This project aims at applying and enhancing existing techniques, as well as developing new algorithms to verify large systems. This project is funded by ASTEC.

People

People involved in this project are:

Projects

FixIt

This project was initiated in collaboration with Chalmers University of Technology and Prover Technology. For information about this project, please go there.

Fault Tree Analysis of dynamic systems

This project is developed in collaboration with Prover Technology within the ESACS project. Its goal is to develop tools to perform Fault Tree Analysis on time-dependent systems.

Fault Tree Analysis is a well-spread method of investigating failures of systems during the design stage. It allows designers to find what combinations of failures of components (called basic events) can lead to a failure of the whole system (called top event). The goal of this project is to incorporate modern model checking techniques into the existing designer's toolbox to allow automated fault tree analysis of time-dependent models.

In a first step, a model of the system is created. It does not yet include failure-related information. At this point, model checking can be used to prove the system's correctness. This means that assuming that all component are perfect (ie: they never fail), we can verify that the system satisfies certain requirements.
Then information about failures of components is added. This information describes what can cause each component to fail. Moreover, it describes the faulty behaviour of the component.
Model checking is again used to verify certain requirements. However the goal here is not to prove that the system still behaves correctly. No system can be fully fault-tolerant. Instead, we want to extract information about the minimal combinations of components failures leading to the violation of the requirement. This information is extracted from the traces returned by the model checker.

Status of Fault Tree Analysis of dynamic systems

A prototype of the analysis tool is implemented as an extension of Prover SL for Esterel Technologies SCADE Suite.
It is accompagnied by a GUI allowing designers to easily extend systems with failure information.

Features currenltly available are:

• Verification of time-dependent boolean systems
• Support for rationals and integers, though not complete
• Report traces describing sequences of failures of components leading to a system failure.

• Ordering information about failures of components
• Support for transient failures