Symbolic Model Checking

by Kenneth L. McMillan

Overview

Formal verification means having a mathematical model of a system, a language for specifying desired properties of the system in a concise, comprehensible and unambiguous way, and a method of proof to verify that the specified properties are satisfied. When the method of proof is carried out substantially by machine, we speak of automatic verification. Symbolic Model Checking deals with methods of automatic verification as applied to computer hardware.
The practical motivation for study in this area is the high and increasing cost of correcting design errors in VLSI technologies. There is a growing demand for design methodologies that can yield correct designs on the first fabrication run. Moreover, design errors that are discovered before fabrication can also be quite costly, in terms of engineering effort required to correct the error, and the resulting impact on development schedules. Aside from pure cost considerations, there is also a need on the theoretical side to provide a sound mathematical basis for the design of computer systems, especially in areas that have received little theoretical attention.

Product Details

ISBN-13:	9781461363996
Publisher:	Springer US
Publication date:	10/23/2012
Edition description:	Softcover reprint of the original 1st ed. 1993
Pages:	194
Product dimensions:	6.10(w) x 9.25(h) x 0.02(d)

Table of Contents

1 Introduction.- 1.1 Background.- 1.2 Scope of this work.- 2 Model Checking.- 2.1 Temporal logic.- 2.2 The temporal logic CTL.- 2.3 Fixed points.- 2.4 CTL model checking.- 3 Symbolic Model Checking.- 3.1 Boolean representations.- 3.2 Symbolic models.- 3.3 Binary Decision Diagrams.- 3.4 Examples.- 3.5 Graph width and OBDDs.- 4 The SMV System.- 4.1 An informal introduction.- 4.2 The input language.- 4.3 Formal semantics.- 5 A Distributed Cache Prool.- 5.1 The Prool.- 5.2 Verifying the prool.- 5.3 Discussion.- 6 Mu-Calculus Model Checking.- 6.1 The Mu-Calculus.- 6.2 Symbolic models.- 6.3 Symbolic algorithm.- 6.4 Applications of the Mu-Calculus.- 6.5 Related research.- 7 Induction and Model Checking.- 7.1 The general framework.- 7.2 Induction and symbolic model checking.- 7.3 Example: The Gigamax prool.- 7.4 Induction in other models.- 7.5 Related research.- 8 Equivalence Computations.- 8.1 State equivalence.- 8.2 Methods for functional composition.- 8.3 Experimental results.- 9 A Partial Order Approach.- 9.1 Unfolding.- 9.2 Truncated unfoldings.- 9.3 Application example.- 9.4 Deadlock and occurrence nets.- 9.5 Conclusion.- 10 Conclusion.- References.