5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 51

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 51)

This is formalized by the LTL formula: ¬ (m ∈ S.out ∧ m ∈ R.in).• The characteristic of FIFO-channels is that they are “order-preserving” according tothe “first in, first out principle” stating that if message m is offered first by S to itsoutput buffer S.out and subsequently m , then m will be received by R before m : m ∈ S.out ∧ ¬ m ∈ S.out ∧ ♦(m ∈ S.out)−→ ♦ (m ∈ R.in ∧ ¬ m ∈ R.in ∧ ♦(m ∈ R.in)) .Note that in the premise the conjunct ¬ m ∈ S.out is needed in order to specifythat m is put in S.out after m.

♦ (m ∈ S.out) on its own does not exclude that mis already in the sender’s buffer when message m is in S.out.The above formulae refer to fixed messages m and m . In order to state the above propertiesfor all messages, we have to take the conjunction over all messages m, m . As long as themessage alphabet is finite we still obtain an LTL formula.Example 5.13.Dynamic Leader Election(This example has been taken from [69].) In current distributed systems several services are offered by some dedicated process(es) in the system. Consider, for example,address assignment and registration, query coordination in a distributed database system,Linear Temporal Logic243clock distribution, token regeneration after token loss in a token ring network, initiationof topology updates in a mobile network, load balancing, and so forth.

Usually manyprocesses in the system are potentially capable of providing these services. However, forconsistency reasons it is usually the case that at any time only one process is allowed toactually provide a given service. This process – called the “leader” – is in fact elected.Sometimes it suffices to elect an arbitrary process, but for other services it is important toelect the process with the best capabilities for performing that service.

Here we abstractfrom specific capabilities and use ranking on the basis of process identities. The idea istherefore that the higher the process’ identity, the better its capabilities.Assume we have a finite number N > 0 of processes connected via some communicationmeans. The communication between processes is asynchronous, as in the previous example.Pictorially,P1P2.

. . . . . .PNCommunication NetworkEach process has a unique identity, and it is assumed that a total ordering exists on theseidentities. Processes behave dynamically in the sense that they are initially inactive, i.e.,not participating in the election, and may become active, i.e., participating in the election,at arbitrary moments. In order to have some progress we assume that a process cannot beinactive indefinitely; that is, each process becomes active at some time. (This correspondsto a fairness condition.) Once a process participates it continues to do so, i.e., it does notbecome inactive anymore. For a given set of active processes a leader will be elected; ifan inactive process becomes active, a new election takes place if this process has a higheridentity than the current leader.To give an idea of using LTL as specification formalism we formulate several propertiesby LTL formulae. We will use i, j as process identities.

Let the set of atomic propositionsbe { leaderi , activei | 1 i, j N }, where leaderi means that process i is a leader, activeimeans that process i is active. An inactive process cannot be a leader.• The property “There is always one leader” can be formalized by !leaderi ∧¬ leaderj .1iN1jNj=i244Linear Temporal LogicAlthough this formula expresses the informally stated property, it will not be satisfiedby any realistic protocol. One reason is that processes may be initially inactive, andthus no leader is guaranteed to exist initially. Besides, in a distributed system withasynchronous communication, switching from one leader to another can hardly bemade atomic.

So, it is more realistic to allow the temporary absence of a leader. Asa first attempt to do so, one could modify the above formula into !leaderi ∧¬ leaderj .ϕ = ♦1iN1jNj=iProblematic, though, is that this allows there to be more than one leader at a timetemporarily – it is only stated that infinitely often there should be exactly oneleader, but no statement is made about the moments at which this is not the case.For consistency reasons this is not desired.

We therefore replace the above formulaϕ with ϕ1 ∧ ϕ2 where ϕ1 and ϕ2 correspond to the following two properties.• “There must always be at most one leader”: ¬ leaderjleaderi →ϕ1 = 1iN1jNj=i• “There will be enough leaders in due time”:!ϕ2 = ♦leaderi1iNϕ2 does not imply that there will be infinitely many leaders. It only states thatthere are infinitely many states at which a leader exists. This requirement classifiesa leader election protocol that never elects a leader to be wrong. In fact, sucha protocol would fulfill the previous requirement, but is not desired for obviousreasons.• “In the presence of an active process with a higher identity the leader will resign atsome time”: ((leaderi ∧ ¬ leaderj ∧ activej ) → ♦ ¬ leaderi )1i,jNi<jFor reasons of efficiency it is assumed not to be desirable that a leader eventuallyresigns in the presence of an inactive process that may participate at some unknowntime in the future.

Therefore we require j to be an active process.Linear Temporal Logic245• “A new leader will be an improvement over the previous one”. This property requiresthat successive leaders have an increasing identity. In particular, a process thatresigns once will not become a leader anymore. (leaderi ∧ ¬ leaderi ∧ ♦leaderj ) → (i < j)1i,jNHere, we use ”i < j” as an atomic proposition that compares the identifiers ofprocesses Pi and Pj and evaluates to true if and only if the process identifier of Piis smaller than that of Pj . Assuming that the identity of Pi is i (for i = 1, .

. . , N ),the above property can also be specified by the LTL formula (leaderi ∧ ¬ leaderi ∧ ♦leaderj ) .¬1i,jNijExample 5.14.Specifying the Input/Output Behavior of Sequential ProgramsThe typical requirements on sequential programs such as partial correctness and termination can “in principle” be represented in LTL. Let us briefly describe what terminationand partial correctness mean. Assume that a sequential program Prog computes a functionof the type f : Inp → Outp, i.e., Prog takes as input a value i ∈ Inp and terminates eitherby reporting an output value o ∈ Outp or does not terminate.

Prog is called terminatingif the computation of Prog halts for each input value i ∈ Inp. Prog is partially correct iffor any input value i ∈ Inp, whenever Prog terminates then the output value o equals f (i).How can termination and partial correctness be expressed by means of LTL formulae?Termination can be specified by a formula of the form init → ♦halt where init is thelabeling for the initial states and halt is an atomic proposition characterizing exactlythose states that stand for termination.

(Without loss of generality it can be assumedthat transition systems have no terminal states, i.e., this means terminating states eitherare equipped with a self-loop, or have a transition leading to a trap-state with a self-loopand no other outgoing transitions.)Partial correctness can be represented by a formula of the form( halt −→ ♦(y = f (x)))where y is the output variable and x the input variable which is assumed not to changeduring program execution. Additional initial conditions such as expressed by the formulainit can be added as premise as follows:init −→ (halt −→ ♦(y = f (x))).246Linear Temporal LogicIt should be stressed that this is an extremely simplified representation.

In practice,predicate logic concepts are needed to precisely formulate partial correctness. And even incases where propositional logic formulae of the above form can be used to exactly describetermination and partial correctness, the algorithmic proof of the LTL formulae is verydifficult or even impossible. (Recall the undecidability of the halting problem.)Remark 5.15.Specifying Timed Properties with LTL for Synchronous SystemsFor synchronous systems, LTL can be used as a formalism to specify “real-time” propertiesthat refer to a discrete time scale.

Recall that in synchronous systems, the involvedprocesses proceed in a lock step fashion, i.e., at each discrete time instance each processperforms a (sometimes idle) step. In this kind of system, the next-step operator has a“timed” interpretation: ϕ states that “at the next time instant ϕ holds”. By puttingapplications of in sequence, we obtain, e.g.:k ϕ = ... ϕdef“ϕ holds after (exactly) k time instants”.k-timesAssertions like “ϕ will hold within at most k time instants” are obtained by! i ϕ.♦k ϕ =0ikStatements like “ϕ holds now and will hold during the next k instants” can be representedas follows:! i ¬ ϕ.k ϕ = ¬ ♦k ¬ ϕ = ¬0ikFor the modulo 4 counter of Example 5.11 (page 240) we in fact already implicitly usedLTL-formulae as real-time specifications.

For example, the formula expressing that oncethe output is y=1, the next three steps the output is y=0:( y −→ ( ¬y ∧ ¬ y ∧ ¬ y) )can be abbreviated as (y −→ 2 ¬ y).It should, however, be noted that the temporal interpretation of the next-step operatoris only appropriate for synchronous systems. Every transition in these systems representsthe cumulative effect of the actions possible within a single time instant.

Характеристики

Список файлов книги