Sriram K. Rajamani
Formal design verification is a methodology for detecting logical errors in systems. In formal design verification, the designer describes a system in a language with a mathematical semantics, and then the system description is analyzed against various correctness requirements. The paradigm is called model checking when the analysis is performed automatically by exhaustive state-space exploration. A correctness requirement is usually specified either as a formula expressed in temporal logic, or as an abstract design expressed in the system's description language. If the requirement is specified as an abstract design, the verification problem is called refinement checking. This thesis extends the state-of-art by increasing both the class, and the size of systems on which automatic and semi-automatic refinement checking are viable.
Refinement checking problems are formulated in the form I < S, where I is a description of the system, S is the requirement, and < is a preorder over system descriptions. Depending on the properties we ascribe to the < preorder, we get different notions of refinement. Three orthogonal property classes characterize the refinement preorder, namely, (1) linear and branching views of time, (2) finite and fair views of system behaviors, and (3) spatial and temporal abstraction of the requirement. We develop the theory of fair branching refinements, and give an efficient algorithm to check such refinements. We propose a novel and efficient algorithm to check refinements involving temporal abstractions.
Refinement checking algorithms usually explore and analyze the state space of the system. As we seek to enhance the applicability of model checking to complex designs, we are faced with the so-called state-explosion problem: the size of the state space grows exponentially with the size of the system description, making exhaustive state-space exploration infeasible. Scalable approaches to refinement checking make use of the compositional structure of both implementation and specification, and divide the verification task at hand into simpler subtasks. Each such subtask involves checking if an implementation-component refines its corresponding specification-component. Discharging such subtasks requires assumptions about inputs to the implementation-component. These assumptions are taken into account by the assume-guarantee approach, which uses the specification for the inputs as assumptions on the inputs (the apparent circularity in such proofs is resolved by an induction over time). We prove soundness of the assume-guarantee rule when applied to branching refinements (both finite and fair cases). We propose a new assume-guarantee proof rule for checking refinements of implementations against requirements that are both spatially and temporally abstract.
The techniques have been implemented in a new verification tool called Mocha. Mocha has been used successfully to detect and fix elusive bugs in a signal-processing chip that has 6 million transistors.
Ph.D. thesis, University of California at Berkeley, September 1999, 142 pages.