176 REAL-TIME LOGIC, GRAPH-THEORETIC ANALYSIS, AND MODECHART

is augmented with lower/upper bound requirements on time separation (distance) between two points along a path starting from the root.

A computation of a system is an assignment of time values, consistent with the lower/upper bound requirements, to the events along a path starting from the root of the tree. Given a pair of points Pa and Pb, with a < b, along a path (so Pa appears earlier than Pb on the path), we represent the lower bound separation requirement as Pa + I ≤ Pb and the upper bound separation requirement as Pb ≤ Pa + I , where I is a non-negative integer.

We can use a weighted directed graph, called a separation graph, to represent the set of time bound separations on a path in a computation tree. In this graph, the nodes are the points in the corresponding path, and the weights associated with the edges indicate the time separation between the nodes.

6.9.2 Computation Graph

Since the above computation tree augmented with lower/upper bound requirements is usually infinite, a need exists to generate a finite computation graph that represents the computations of the system [Jahanian and Stuart, 1988] so that model checking or similar verification techniques can be applied to it. To derive a finite computation graph from an infinite computation tree, we use a point Pa that is already generated instead of generating a new one Pb (as in the case of the computation tree) if Pa is equivalent to Pb except for their time stamps. In other words, an infinite number of equivalent points are grouped together into an equivalence class. Since a finite number of equivalence classes exist in the point space of a Modechart specification, we can obtain a finite computation graph by generating at most one point from each equivalence class.

The computation graph construction algorithm starts by generating the root point of the computation graph. Then it checks every transition from the active modes in the root point to if see it can be taken. As discussed before, a transition can occur if it satisfies its associated triggering or timing condition. If a transition can be taken, the algorithm generates a new point (successor to the root point) if it is not in the same equivalence class as the root point, and this transition and this new point are added to the computation graph. The above steps are repeated in a breadth-first exploration for every new point until no new points can be included in the computation graph. Note the similarity of this construction and the generation of a finite-state graph to a program described in chapter 4.

6.9.3 Timing Properties

We now describe two practical classes of timing properties expressed in RTL for which simple verification procedures are available to check their satisfiability in a computation graph [Jahanian and Stuart, 1988]. The following definitions are needed to specify these properties.

VERIFYING TIMING PROPERTIES OF MODECHART SPECIFICATIONS

177

Endpoint: Given an event E, an integer variable i, and a non-negative integer constant k, an endpoint is an application of an occurrence function of the form @(E, i ± k).

Note that in this form, the expression i ± k is the occurrence index of this occurrence function application.

Related Endpoints: If the integer variables appearing in the occurrence indices of a pair of endpoints’ occurrence function applications are the same, then these two endpoints are related.

For example, @(E1, x) and @(E2, x + 8) are related endpoints.

Interval: Given two events E1 and E2, two non-negative integer constants k1 and k2, and an integer variable i, an interval is a pair of related endpoints of the form @(E1, i ± k1) and @(E2, i ± k2).

Recall that a computation graph uses one point to represent an equivalence class of an infinite number of points, and the events happening in these points are usually different instances of the same event. Therefore, if a cycle exists whose points are labeled with the same number of events E1 and E2 in the computation graph, then by marking an E1-labeled point as its ith occurrence, we can traverse this cycle forward or backward a constant number of times to locate the point representing the ith occurrence of event E2, depending on whether this occurrence of E2 follows or precedes, respectively, the ith occurrence of event E1.

Preservation of Related Endpoints: Given a computation graph G and a pair of related endpoints with events E1 and E2, a cycle preserves this pair of endpoints if in this cycle the number of E1-labeled points is equal to the number of E2-labeled points.

Preservation of an RTL Formula: If every cycle in a computation graph preserves every pair of related endpoints in an RTL formula, then this graph preserves this formula.

We can check in polynomial time whether two endpoints are preserved by a computation graph, but the following cases can be checked by inspection. A computation preserves a pair of endpoints containing events E1 and E2 if one of the following cases is true:

1.E1 = E2, that is, they are the same event.

2.E1 =→ M and E2 = M →, that is, these events are the entry and exit events of the same mode.

3.E1 = (S := true) and E2 = (S := false), that is, these events are transition events of the same state variable.

178REAL-TIME LOGIC, GRAPH-THEORETIC ANALYSIS, AND MODECHART

4.E1 = ↑A and E2 = ↓A, that is, these events are the start and stop events of the same action.

Next we describe two classes of RTL formulas that are preserved by a computation graph. Simple procedures are available for determining whether a computation graph satisfies a property in one of these classes.

6.9.4 Minimum and Maximum Distance Between Endpoints

This class of timing properties specifies the relative and absolute ordering as well as the time distance between related endpoints. Given two related endpoints e1 and e2 and a non-negative integer time distance k, the RTL formulas expressing these timing properties are of the form x F or x F, where F is a quantifier-free formula with each inequality of the form

e1 ± k ≤ e2.

Each inequality can be rewritten as one of the following to specify:

1.The minimum time distance k between two endpoints: k ≤ e2 − e1.

2.The maximum time distance k between two endpoints: e1 − e2 ≤ k.

We now present the minimum and maximum distance algorithms for two related endpoints. Their functions and operations are similar to the minimum and maximum delay algorithms [Campos et al., 1994] presented in chapter 4, but cycle unrolling is required here since a point may correspond to an equivalence class of points representing different time-stamped occurrences of the same event.

Let G be the computation graph and F be the RTL formula specifying minimum distances between endpoints. The following algorithm (Figure 6.6) determines if every computation in G satisfies the minimum-distance timing property specified in F.

The following algorithm (Figure 6.7) determines if every computation in G satisfies the maximum-distance timing property specified in F.

If the formula F is universally quantified, then we run the appropriate algorithm above for every E j -labeled point in the graph G, and each run must return true for G to satisfy F. Otherwise, if the formula F is existentially quantified, then at least one

procedure check min distance(e1, e2, k, G, F)

find a point P labeled with E j , where 1 ≤ j ≤ n;

find all corresponding endpoints in F by unrolling each cycle a constant number of times;

d := shortest distance between e1 and e2 in unrolled G; if k ≤ d then return true else return false;

Figure 6.6 Algorithm for checking minimum distance.

VERIFYING TIMING PROPERTIES OF MODECHART SPECIFICATIONS

179

procedure check max distance(e1, e2, k, G, F)

find a point P labeled with E j , where 1 ≤ j ≤ n;

find all corresponding endpoints in F by unrolling each cycle a constant number of times;

d := longest distance between e1 and e2 in unrolled G; if d ≤ k then return true else return false;

Figure 6.7 Algorithm for checking maximum distance.

run of the appropriate algorithm above for an E j -labeled point in the graph G must return true for G to satisfy F.

6.9.5 Exclusion and Inclusion of Endpoint and Interval

This class of timing properties specifies the exclusion or inclusion of an endpoint or an interval within another interval. Here we add an integer offset to an endpoint: @(E, i ± k) ± c.

Given an interval I1 with endpoints e1 and e2 and an interval I2 with endpoints e3 and e4, the RTL formulas expressing the timing properties in this class are in one of the two forms.

Let Qa and Qb be quantifiers on the interval occurrence index variables. The first form describes that an interval includes another:

Qa Qbe1 ≤ e3 e4 ≤ e2.

For example, this RTL formula states that while mode PASSED is active, an execution of the action Upgate begins after entering this mode 10 s or later:

x y@(→ PASSED, x) + 10 ≤ @(↑ Upgate, y) @(↓ Upgate, y)

≤ @(M →, x).

The second form describes that an interval excludes another:

Qa Qbe4 ≤ e1 e2 ≤ e3.

For example, this RTL formula states that actions Upgate and Downgate are mutually exclusive:

x y@(↓ Downgate, y) ≤ @(↑ Upgate, x) @(↓ Upgate, x)

≤ @(↑ Downgate, y).

The algorithm to determine whether a computation graph satisfies a given RTL formula specifying a timing property in this class depends on the combination of quantifiers in Qa and Qb as well as on whether it is an inclusion or exclusion prop-