Database of Case Studies Achieved Using CADP

Model-Based Diagnosis using LNT

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


Last modified: Thu May 2 14:18:40 2019.


Back to the CADP case studies page