Model-based Diagnosis Patterns for Model Checking

Vincent Leilde (1, 2) , Vincent Ribaud (3) , Philippe Dhaussy (1, 2)

1 Lab-STICC_ENSTAB_CACS_MOCS
2 Pôle STIC_IDM
3 Lab-STICC_UBO_CACS_MOCS

Verification process including model checking is a technique used to verify that a certain system's design satisfies its requirements. It relies on a large collection of heterogeneous artifacts and diagnosing faults is generally a tedious task which should benefit from a knowledge base system to collect and provide access to well-formalized verification artifacts. In the formal method community there is no common agreement on a formalization or organization for the whole verification process artefacts, such as models, traces or sessions of verifications. Hence this paper asks the question about unmet needs for such patterns and their possible relationships, with a particular focus on patterns required for diagnosis techniques such as Model Based Diagnosis or Case Based Diagnosis.

Mots clés: Patterns; Model Checking; Diagnosis; Organizing system

Domaines: Modélisation et simulation; Génie logiciel [cs.SE]

Vincent Leilde, Vincent Ribaud, Philippe Dhaussy. Model-based Diagnosis Patterns for Model Checking. PAME 2016, Oct 2016, St Malo, France. pp.7-12. ⟨hal-01406604⟩