5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 32
Текст из файла (страница 32)
It may be necessary to impose fairness assumptions on the environment in order to be able to verify liveness properties, such as “thevalues 0 and 1 are output infinitely often”. Let us illustrate this by means of a concrete example. Consider a sequential circuit with input variable x, output variable y, and registerr. Let the transition function and the output function be defined asλy = δr = x ↔ ¬r.That is, the circuit inverts the register and output evaluation if and only if the input bitis set.
If x=0, then the register evaluation remains unchanged. The value of the registeris output. Suppose all transitions leading to a state with a register evaluation of the form[r = 1, . . .] are labeled with the action set. Imposing the unconditional fairness assumption{{ set }} ensures that the values 0 and 1 are output infinitely often.3.5.3Fairness and SafetyWhile fairness assumptions may be necessary to verify liveness properties, they are irrelevant for verifying safety properties, provided that they can always be ensured by means ofan appropriate scheduling strategy. Such fairness assumptions are called realizable fairnessassumptions.
A fairness assumption cannot be realized in a transition system wheneverthere exists a reachable state from where no fair path begins. In this case, it is impossibleto design a scheduler that resolves the nondeterminism such that only fair paths remain.Example 3.53.A Nonrealizable Fairness AssumptionConsider the transition system depicted in Figure 3.13, and suppose the unconditionalfairness assumption { { α } } is imposed.
As the α-transition can only be taken once, it isevident that the transition system can never guarantee this form of fairness. As there isa reachable state from which no unconditional fair path exists, this fairness assumption isnonrealizable.Definition 3.54.Realizable Fairness AssumptionLet TS be a transition system with the set of actions Act and F a fairness assumption forAct.
F is called realizable for TS if for every reachable state s: FairPathsF (s) = ∅.140Linear-Time Propertiesα∅aFigure 3.13: Unconditional fairness.Stated in words, a fairness assumption is realizable in a transition system TS whenever inany reachable state at least one fair execution is possible. This entails that every initialfinite execution fragment of TS can be completed to a fair execution.
Note that there isno requirement on the unreachable states.The following theorem shows the irrelevance of realizable fairness assumptions for theverification of safety properties. The suffix property of fairness assumptions is essential forits proof. This means the following. Ifα1α2α3→ s1 −−→ s2 −−→ ...ρ = s0 −−is an (infinite) execution fragment, then ρ is fair if and only if every suffixαααj+1j+2j+3−→ sj+1 −−−−→ sj+2 −−−−→ . .
.sj −−−of ρ is fair too. Conversely, every fair execution fragment ρ (as above) starting in state s0can be preceded by an arbitrary finite execution fragmentβ1β2βn→ s1 −−→ . . . −−→ sn = s0s0 −−ending in s0 . Proceeding in s0 by execution ρ yields the fair execution fragment:β1β2βnα1α2α3→ s1 −−→ . . . −−→ sn = s0 −−→ s1 −−→ s −−→ ...s0 −− 2 arbitrary starting fragmentTheorem 3.55.fair continuationRealizable Fairness is Irrelevant for Safety PropertiesLet TS be a transition system with set of propositions AP, F a realizable fairness assumption for TS, and Psafe a safety property over AP.
Then:TS |= Psafeif and only ifTS |=F Psafe .Proof: “⇒”: Assume TS |= Psafe . Then, by definition of |= and the fact that the fairtraces of TS are a subset of the traces of TS, we haveFairTracesF (TS) ⊆ Traces(TS) ⊆ Psafe .Summary141Thus, by definition of |=F it follows that TS |=F Psafe .“⇐”: Assume TS |=F Psafe . It is to be shown TS |= Psafe , i.e., Traces(TS) ⊆ Psafe .This is done by contraposition.
Let σ ∈ Traces(TS) and assume σ ∈/ Psafe . As σ ∈ Psafe ,there is a bad prefix of σ, σ say, for Psafe . Hence, the set of properties that has σ as aprefix, i.e.,ω| σ ∈ pref(σ ) ,P = σ ∈ 2AP = s0 s1 . . . sn be a finite path fragment of TS withsatisfies P ∩ Psafe = ∅.
Further, let πtrace(π) = σ.Since F is a realizable fairness assumption for TS and sn ∈ Reach(TS), there is an F-fairpath starting in sn . Letsn sn+1 sn+2 . . . ∈ FairPathsF (sn ).The path π = s0 . . . sn sn+1 sn+2 . . . is in FairPathsF (TS) and thus,trace(π) = L(s0 ) . . . L(sn ) L(sn+1 ) L(sn+2 ) . . . ∈ FairTracesF (TS) ⊆ Psafe .On the other hand, σ = L(s0 ) . . . L(sn ) is a prefix of trace(π). Thus, trace(π) ∈ P . Thiscontradicts P ∩ Psafe = ∅.Theorem 3.55 does not hold if arbitrary (i.e., possibly nonrealizable) fairness assumptionsare permitted. This is illustrated by the following example.Example 3.56.Nonrealizable Fairness may harm Safety PropertiesConsider the transition system TS in Figure 3.14 and suppose the unconditional fairnessassumption F = { { α } } is imposed.
F is not realizable for TS, as the noninitial state(referred to as state s1 ), is reachable, but has no F-fair execution. Obviously, TS hasonly one fair path (namely the path that never leaves the initial state s0 ). In contrast,paths of the form s0 . . . s0 s1 s1 s1 . . .
are not fair, since α is only executed finitely often.Accordingly, we have thatTS |=F “never a”3.6butTS |= “never a”.Summary• The set of reachable states of a transition system TS can be determined by a searchalgorithm on the state graph of TS.142Linear-Time Properties∅{a}αβFigure 3.14: Unconditional fairness may be relevant for safety properties.• A trace is a sequence of sets (!) of atomic propositions. The traces of a transitionsystem TS are obtained from projecting the paths to the sequence of state labels.• A linear-time (LT, for short) property is a set of infinite words over the alphabet2AP .• Two transition systems are trace-equivalent (i.e., they exhibit the same traces) ifand only if they satisfy the same LT properties.• An invariant is an LT property that is purely state-based and requires a propositionallogic formula Φ to hold for all reachable states.
Invariants can be checked usinga depth-first search where the depth-first search stack can be used to provide acounterexample in case an invariant is refuted.• Safety properties are generalizations of invariants. They constrain the finite behaviors. The formal definition of safety properties can be provided by means of theirbad prefixes in the sense that each trace that refutes a safety property has a finiteprefix, the bad prefix, that causes this.• Two transition systems exhibit the same finite traces if and only if they satisfy thesame safety properties.• A liveness property is an LT property if it does not rule out any finite behavior. Itconstrains infinite behavior.• Any LT property is equivalent to an LT property that is a conjunction of a safetyand a liveness property.• Fairness assumptions serve to rule out traces that are considered to be unrealistic.They consist of unconditional, strong, and weak fairness constraints, i.e., constraintson the actions that occur along infinite executions.• Fairness assumptions are often necessary to establish liveness properties, but theyare—provided they are realizable—irrelevant for safety properties.Bibliographic Notes3.7143Bibliographic NotesThe dining philosophers example discussed in Example 3.2 has been developed by Dijkstra [128] in the early seventies to illustrate the intricacies of concurrency.
Since then ithas become one of the standard examples for reasoning about parallel systems.The depth-first search algorithm that we used as a basis for the invariance checking algorithm goes back to Tarjan [387]. Further details about graph traversal algorithms canbe found in any textbook on algorithms and data structures, e.g. [100], or on graphalgorithms [188].Traces. Traces have been introduced by Hoare [202] to describe the linear-time behaviorof transition systems and have been used as the initial semantical model for the process algebra CSP. Trace theory has further been developed by, among others, van deSnepscheut [403] and Rem [354] and has successfully been used to design and analyzefine-grained parallel programs that occur in, e.g., asynchronous hardware circuits.
Several extensions to traces and their induced equivalences have been proposed, such as failures [65] where a trace is equipped with information about which actions are rejected afterexecution of such trace. The FDR model checker [356] supports the automated checkingof failure-divergence refinement and the checking of safety properties.
A comprehensivesurvey of these refined notions of trace equivalence and trace inclusion has recently beengiven by Bruda [68].Safety and liveness. The specification of linear-time properties using sets of infinite sequences of states (and their topological characterizations) goes back to Alpern and Schneider [5, 6, 7]. An earlier approach by Gerth [164] was based on finite sequences. Lamport [257] categorized properties as either safety, liveness, or properties that are neither.Alternative characterizations have been provided by Rem [355] and Gumm [178]. Subclasses of liveness and safety properties in the linear-time framework have been identifiedby Sistla [371], and Chang, Manna, and Pnueli [80].
Other definitions of liveness properties have been provided by Dederichs and Weber [119] and Naumovich and Clarke [312](for linear-time properties), and Manolios and Trefler [285, 286] (for branching-time properties). A survey of safety and liveness has been given by Kindler [239].Fairness. Fairness has implicitly been introduced by Dijkstra [126, 127] by assumingthat one should abstract from the speed of processors and that each process gets its turnonce it is initiated. Park [321] studied the notion of fairness in providing a semanticsto data-flow languages. Weak and strong fairness have been introduced by Lehmann,Pnueli, and Stavi [267] in the context of shared variable concurrent programs.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
