Symbolic Model Checking
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 involved in this project are:
This project was initiated in collaboration with Chalmers University of Technology and Prover Technology. For information about this project, please go there.
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
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.
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: