Systems running the SpaceWire protocol are synchronous, meaning that state machine transitions occur on the ticks of the system clock. Depending on whether the ErrorReset state should be entered immediately on the next tick after one of the three conditions becomes true, or on some subsequent clock tick. As the name suggests, temporal logic is a precise mathematical notation with associated rules for representing and inferring the temporal properties of systems.

While temporal logic has been used by philosophers and logicians since the time of Aristotle, only in the last thirty years has it found application as a mathematical notation for specifying system requirements. We will first introduce the notion of an invariant and then generalize it to more expressive specifications in temporal logic.

## Invariants

Both of the above properties of the SpaceWire protocol are invariant, although this may not be immediately obvious. Below is an example of an invariant property of the model we encountered in Chapter 3. It is also desirable to determine the invariant properties of the software and hardware implementation of embedded systems.

For this example, it is required that the value of the desired climb variable remains within the range [- CLIMBMAX, CLIMBMAX] at the end of altitude control task. This is an example of a special kind of invariant, a post condition, that must be maintained every time height control task returns.

## Linear Temporal Logic

### Propositional Logic Formulas

The proposition is true at a reactionqi ifqi = (x,b,y) for any valuationxandy, which means that the machine is in state at the start of the reaction. Propositions for the state machines in Figure 13.1 include any of the above atomic propositions and expressions using the logical connections along with atomic propositions. In other words, if we want to state that p1 =⇒ p2 is true, it is equally valid to state that ¬p2 =⇒ ¬p1 is true.

### LTL Formulas

In mathematical notation, Gφ holds for the trace if and only if, for allj ≥0, formulaφ in the suffix qj, qj+1, qj+2, holds. Example 13.6: In Figure 13.1(b) G(x =⇒ y) is true for all tracks of the machine, and therefore holds for the machine. G(x∧y) does not hold for the machine because it is false for any trace where it is absent in any reaction. Formally, Fφ holds for the trace if and only if, forsomej ≥ 0, formulaφ in the suffix qj, qj+1, qj+2, holds.

Example 13.8: In Figure 13.1(a), x =⇒ Xa holds for the state machine, because if xi is present in the first reaction, then the next state is a.G(x. Formally, φ1Uφ2 holds for the trace if and only if there existsj ≥0 such that φ2 holds in the suffix qj, qj+1, qj+2,.

### Using LTL Formulas

This property is of the form G Fp, which means that it is always the case that eventually it works. This property is of the form F Gp, read as "from some time in the future, holds at all times". This represents a steady-state property, indicating that after some time the system reaches a steady state in which it is always true.

## Summary

More formally, a property p is a safety property if a system implementation does not satisfy if and only if there exists a finite-length prefix of the implementation that cannot be extended to an infinite implementation that satisfies p. In the above example, if the ISR must be executed within 100 clock cycles of the interrupt being asserted, the property is a bounded lifetime property; otherwise, if there is no such time bound to the occurrence of the ISR, it is an unlimited living property. Give a short answer and motivation for each of the following questions. a) TRUE or FALSE: If GF holds for a state machine A, then FGp also holds.

For each of the following LTL formulas, determine whether they are true or false, and give a counterexample if they are false:. The following temporal logic formula is satisfied by the sequence w for every possible behavior of the composition and not by any sequence that is not a behavior of the composition:.

Models as Specifications

## Type Equivalence and Refinement

The inputs have typeVx andVw, which means that at the action of the actor, the values of the input members of the sets will be VxorVw. Let the type of an output port q ∈ QA be Vq, and the type of the corresponding output port q∈QBbeVq0. If B is a type refinement of A, substituting AbyB in any environment will not cause type system problems.

They have the same input and output ports, and the port types are the same. The ports and their types are identical for both machines, so they are type equivalent.

## Language Equivalence and Containment

Like deterministic machines, two nondeterministic machines are linguistically equivalent if they share the same language. In the above example, in all behaviors in La(M), the output is present a limited number of times, in the same reactions when the input is present. For example, the + operator means "one or more", in contrast to the Kleene asterisk, which means "zero or more". For example, a+ specifies the sequence, aa, aaa, etc.; it's the same asa(a*).

It can produce any output sequence that M1 and M2 can produce, but it can also produce other outputs with the same inputs. In fact, language containment does not require that the state machines have the same states, so an LTL formula that refers to the states of one machine may not even apply to the other machine.

## Simulation

*Simulation Relations**Formal Model**Transitivity**Non-Uniqueness of Simulation Relations**Simulation vs. Language Containment*

In the next section, we will see that language retention is not good with respect to LTL formulas relating to the states of state machines. Suppose we build each of the two machines with its own copy of the environment that M2 finds acceptable. In the first reaction where it is present, M1 has no choice but to make a transition to the state band and produce an output = 0.

If M1 can observe the state of M2 when it makes its choice, then in the second reaction, where present, it can choose a transition that M2. What it means for M1 to be acceptable in the environment is that whatever decisions it makes are acceptable. In the above example, we can think of the machines maliciously trying to make M1.

Note that machines do not need to know the future; it is enough to simply have good visibility of the present. Then a simulation linkS ⊆S2×S1 is a set of pairs of states occupied by the two machines in each round of the game for all possible inputs. First note that the pair (e,a) of initial states is in the relation, so the relation includes the state of the two cars in the first round.

Note the order here; the machine that moves first in the game, M2, the one being simulated, is the first in States2×States1. Otherwise, if from statecit always chooses to return to stateb, then so is the simulation relation. To see this, keep in mind that M2's language is a strict subset of M3's language.

## Bisimulation

It is important to understand what the sentence says and what it does not say. In fact, this statement is not true, as we have already shown with the examples in Figure 14.3. The two machines are observably different despite their input/output behavior being the same.

The machine that moves second must be able to match all of its possible choices. In this case, the machines may end up in a state where one machine can no longer match all of the other's possible moves. In the next round, if M1 gets to move first, then M2 can no longer match all his possible moves.

Note that this argument does not undermine the finding that these machines simulate each other. If in each round M2 always moves first, M1 will always be able to match each of his moves. Similarly, if M1 moves first in each round, M2 can always match each of its moves (by always moving to j in the first round).

To ensure that two machines are obviously identical in all environments, we need a stronger equivalence relation called bisimulation. We say that M1isbisimilartoM2 (or M1 bisimulates M2) if we can play the modified matching game so that in each round either machine can move first. As in Section 14.4.2, we can use the formal model of nondeterministic FSMs to define a bisimulation relation.

## Summary

We first consider a special case of the model control problem which is useful in practice. The system may have a large number of states, possibly exponential in the size of the syntactic description of M. Therefore, the DFS Search procedure terminates, and the value of R at the end of the procedure is the set of all reachable states of M.

The space and time requirements of this algorithm are linear in the size of the state graph (see Appendix B for an introduction to such complexity concepts). However, the number of nodes and edges in the state graph of M can be exponential in the size of the descriptions of S and E. Letvl be a variable that indicates the state of the traffic light controller FSMSi at the start of each reaction; i.e. vl∈ {green, yellow, red, pending}.

The part of the system to be abstracted depends on the property to be checked. Additionally, notice that the size of the state space to be explored has been reduced to a simple 2n. The properties of the Fp shape, although those of liveness, can be partially verified using the techniques presented earlier in this chapter.

Software execution time is an example of a quantitative property of an embedded system. A major source of complexity in runtime analysis (and other program analysis problems as well) is that the number of program paths can be very large—exponential in the size of the program. We now discuss how properties of the execution platform, particularly cache memory, can significantly affect execution time.

The main assumption we make in this section is that we know. an upper bound wi on the execution time of the basic block i. Adding such bounds to values of xi does not change the complexity of the optimization problem. 9 int check_password(int uid, int pwd) {. a) Draw the control flow chart of the function check password.

Assume that the client knows the program but not the contents of the array all pwds.