Hoque, Khaza Anuarul; Mohamed, Otmane Ait; Abed, Sa'ed et Boukadoum, Mounir
(2012).
« MDG-SAT: an automated methodology for efficient safety checking ».
International Journal of Critical Computer-Based Systems, 3(1/2), pp. 4-25.
Fichier(s) associé(s) à ce document :
Résumé
Multiway decision graph (MDG) is a canonical representation of a
subset of many-sorted first-order logic. It generalises the logic of equality with abstract types and uninterpreted function symbols. The area of satisfiability(SAT) has been the subject of intensive research in recent years, with significant theoretical and practical contributions. In this paper, we propose a new design verification tool integrating MDG and SAT, to check the safety of a design by invariant checking. Using MDG to encode the set of states provides a
powerful mean of abstraction. We use a SAT solver to search for paths of reachable states violating the property under certain encoding constraints. In addition, we introduce an automated conversion-verification methodology to convert a directed formula (DF) into a conjunctive normal form (CNF) formula that can be fed to a SAT solver. The formal verification of this conversion is conducted within the HOL theorem prover. Finally, we present experimental results and a case study to show the correctness and the efficiency of our proposed methodology.
Altmetric
Altmetric
RECHERCHER
PARCOURIR
LIBRE ACCÈS
