lavish
发表于 2025-3-23 12:21:03
http://reply.papertrans.cn/89/8850/884959/884959_11.png
BOON
发表于 2025-3-23 17:01:57
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.
失眠症
发表于 2025-3-23 19:49:48
http://reply.papertrans.cn/89/8850/884959/884959_13.png
Mitigate
发表于 2025-3-24 01:22:14
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).
确定的事
发表于 2025-3-24 05:55:38
http://reply.papertrans.cn/89/8850/884959/884959_15.png
Pessary
发表于 2025-3-24 07:58:44
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
发表于 2025-3-24 12:33:15
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
发表于 2025-3-24 16:05:00
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.
小木槌
发表于 2025-3-24 21:44:59
http://reply.papertrans.cn/89/8850/884959/884959_19.png
Lacerate
发表于 2025-3-25 00:01:53
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 ..