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.

Full Product Details

Author:   Kenneth L. McMillan
Publisher:   Springer-Verlag New York Inc.
Imprint:   Springer-Verlag New York Inc.
Edition:   Softcover reprint of the original 1st ed. 1993
Dimensions:   Width: 15.50cm , Height: 1.20cm , Length: 23.50cm
Weight:   0.338kg
ISBN:  

9781461363996

ISBN 10:   1461363993
Pages:   194
Publication Date:   23 October 2012
Audience:   Professional and scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   Manufactured on demand  
We will order this item for you from a manufactured on demand supplier.

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 Protocol.- 5.1 The Protocol.- 5.2 Verifying the protocol.- 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 protocol.- 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.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions