Titlebook: Systems and Software Verification; Model-Checking Techn Béatrice Bérard,Michel Bidoit,Pierre McKenzie Book 2001 Springer-Verlag Berlin Heid

lavish

BOON

Symbolic Model CheckingGenerally speaking, . refers to any model checking method which would attempt to represent symbolically (as opposed to “explicitly”) the states and transitions of an automaton targeted for verification. We often use this term, as well, to refer to a particular symbolic method in which . (BDD) are used to represent the state variables.

失眠症

Mitigate

Safety PropertiesExamples are everywhere, most often without conditions: “both processes will never be in their critical section simultaneously .” (S1), or “memory overflow will never occur” (S2), or “the situation.. is impossible” (S3). An example of safety with condition is “as long as the key is not in the ignition position, the car won’t start” (S4).

确定的事

Pessary

Deadlock-freenessDeadlock-freeness is a special property, stating that the system can never be in a situation in which no progress is possible. This is a correctness property relevant for systems that are supposed to run indefinitely. In a more general framework, a set of properly identified final states will be required to be deadlock-free.

Panther

Fairness PropertiesAgain here examples abound: “the gate will be raised infinitely often” (F1), “if access to a critical section is infinitely often requested, then access will be granted infinitely often” (F2), etc. Remember that (F2) did not hold for the printer manager from section 1.3.

Agronomy

Abstraction MethodsBy “abstraction methods” we mean a family of techniques which are used to simplify automata. The term . refers to the nature of the simplifications performed, which generally consist in ignoring some aspects of the automaton involved.

小木槌

Lacerate

SPIN — Communicating Automata. is a tool mainly developed by G. J. Holzmann at Bell Labs, Murray Hill, New Jersey, USA. SPIN was designed for simulation and verification of distributed algorithms It is freely available via Internet ..