Titlebook: Symbolic Model Checking; Kenneth L. McMillan Book 1993 Kluwer Academic Publishers 1993 VLSI.computer.design.model.model checking.verificat

光明正大

魔鬼在游行

Book 1993le and unambiguous way, and a method of proofto verify that the specified properties are satisfied. When the methodof proof is carried out substantially by machine, we speak ofautomatic verification. .Symbolic Model Checking. deals withmethods of automatic verification as applied to computerhardware

euphoria

斑驳

Model Checking, more generally, a class of possible imaginary universes. To make our model meaningful, we require a . that predicts some or all of the possible observations that might be made of the model. An observation generally takes the form of the truth or falsehood of a predicate, or statement about the mode

Bureaucracy

Symbolic Model Checking,racterized as fixed points of certain continuous functionals in the lattice of subsets, and how these fixed points can be computed iteratively. This provides us with a model checking algorithm for CTL, but requires us to build a finite Kripke model for our system and hence leads us to the state expl

放牧

The SMV System,l (., a gate level schematic is probably not a high enough level). For our purposes, this means the language must provide operations on suitable high level types (such as symbolic enumerated types), and must allow us to conveniently describe non-deterministic choices, so that we can describe high le

llibretto

A Distributed Cache Protocol,for their Gigamax distributed multiprocessor [MS91]. This protocol is of interest as a test case for automatic verification for two reasons. First, it is not a theoretical exercise, but a real design, which is driven by considerations of performance and economics, as well as the usual constraints of

resilience

Mu-Calculus Model Checking,ties of transition systems, such as reachable state sets, state equivalence relations, and language containment between automata. A symbolic model checking algorithm for this logic allows all of these properties to be computed using OBDDs [BCM.90].

意见一致

Induction and Model Checking,ms of this type are commonplace — they occur in bus protocols and network protocols, I/O channels, and many other structures that are designed to be extensible by adding similar components. In particular, we are interested in verifying properties that hold independent of the number of components in

adipose-tissue

Equivalence Computations,hines, or between states of the same machine. In the former case, the relation can be used to determine the equivalence of the two machines, while in the latter case, as Lin . have observed [LTN90], the self equivalence relation can be used in optimizing the logic or register usage of the machine.