Model-based Diagnosis Patterns for Model Checking

Overview & Synopsis

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.