|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
CONVECS project-team, Inria Grenoble - Rhône-Alpes and LIG
Graz University of Technology (AUSTRIA) |
|---|---|
| Method: |
LNT
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
Component-based Systems.
|
| Period: |
2018
|
| Size: |
up to 473,316 states and 3,204,445 transitions
|
| Description: |
Despite its advantages, model-based diagnosis is not yet often used in
practice. A possible reason is the modeling effort, in particular if
it is unclear whether the chosen modeling formalism offers the right
means for model-based diagnosis. This case study presents an approach
to model-based diagnosis for models written in LNT, a modern formal
modeling language, designed with formal verification in mind.
The basic idea is to make an LNT model usable for diagnosis is to encapsulate components of the system inside wrapper components (written in LNT), a parameter of which controls whether a component behaves correctly or not, i.e., whether it behaves according to the original LNT model, or whether a simulator can use all domain values for the component's parameters. The behaviour of the whole system is obtained by the parallel composition of all wrapper components, following the same architecture as the original LNT model. Fault diagnosis requires to check whether a faulty trace is included in a model with some faulty components. This check can be expressed as an equivalence checking (using BISIMULATOR) or model checking (using EVALUATOR, expressing the faulty trace as a temporal logic formula). This check can be easily integrated into classical diagnosis algorithms, such as Hitting Set Directed Acyclic Graph), either by encoding the diagnosis algorithm in an SVL script, or by connecting an existing algorithm to the CADP toolbox (implementing consistency checks by system calls to CADP). The approach is illustrated on the d74 circuit (frequently used in the literature on fault diagnosis) and an asynchronous model of the DES (Data Encryption Standard), where it was possible to determine all the manually introduced faults using the proposed approach. |
| Conclusions: |
LNT can also be used for fault diagnosis, increasing the possible
benefits and application of a formal model.
|
| Publications: |
[Hofer-Mateescu-Serwe-Wotawa-18]
Birgit Hofer, Radu Mateescu, Wendelin Serwe, and Franz Wotawa.
"Using LNT Formal Descriptions for Model-Based Diagnosis".
Proceedings of the 29th International Workshop on Principles of
Diagnosis (DX'2018), Warsaw, Poland, pages 1-8, August 2018.
Available on-line at http://ceur-ws.org/Vol-2289/paper2.pdf or from http://cadp.inria.fr/publications/Hofer-Mateescu-Serwe-Wotawa-18.html |
| Contact: | Radu Mateescu Inria - LIG / CONVECS 655, avenue de l'Europe CS 90051 38334 Montbonnot FRANCE Email: Radu.Mateescu@inria.fr |
| Further remarks: | This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page