Title: MDG-SAT: an automated methodology for efficient safety checking

Authors: Khaza Anuarul Hoque; Otmane Ait Mohamed; Sa'ed Abed; Mounir Boukadoum

Addresses: Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisooneve Blvd. W, Montreal, Quebec H3G 1M8, Canada. ' Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisooneve Blvd. W, Montreal, Quebec H3G 1M8, Canada. ' Department of Computer Engineering, Hashemite University, P.O. Box 150459, Zarqa 13115, Jordan. ' Department of Computer Science, University of Quebec at Montreal, CP. 8888, Succ. Centre-Ville, Montreal, QC H3P 3P8, Canada

Abstract: 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.

Keywords: satisfiability; SAT; invariant checking; model checking; multiway decision graphs; MDG; conjunctive normal form; CNF conversion; safety checking; design verification; design safety.

DOI: 10.1504/IJCCBS.2012.045074

International Journal of Critical Computer-Based Systems, 2012 Vol.3 No.1/2, pp.4 - 25

Published online: 16 Aug 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article