LCF-style for Secure Verification Platform based on Multiway Decision Graphs.
Sa’ed Abed, Otmane Aı̈t Mohamed · CIIA · 2009
Formal verification of digital systems is achieved, today, using one of two main approaches: states exploration (mainly model checking and equivalence checking) or deductive reasoning (theorem proving). Indeed, the combination of the two approaches, states exploration and deductive reasoning promises to overcome the limitation and to enhance the capabilities of each. A comparison between both categories is discussed in details. In this paper, we are interested in presenting as an example a platform for Multiway Decision Graphs (MDGs) in LCF-style theorem prover. Based on this platform, many conversions such as the reachability analysis and reduction techniques can be implemented that uses the MDG theory within the HOL theorem prover. The paper also questions the best formalization principle of decision graphs to build such a platform in theorem proving since a set of basic operations are used to efficiently manipulate the decision graphs which constitute the kernel of the model checking algorithms, by describing two alternatives to formalize these decision graphs. Then we contrast between them according to their efficiency, complexity and feasibility. Finally, we hope this paper to serve as an adequate introduction to the concepts involved in formalization and a survey of relevant work.