Unifying proof methodologies of duration calculus and timed linear temporal logic.
Linear temporal logic (LTL) has been widely used for specification and verification of reactive systems. Its standard model is sequences of states (or state transitions), and formulas describe sequencing of state transitions. When LTL is used to model real-time systems, a state is extended with a time stamp to record when a state transition takes place. Duration calculus (DC) is another well studied approach for real-time systems development. DC models behaviours of a system by functions from the domain of reals representing time to the system states. This paper extends this time domain to the Cartesian product of the real and the natural numbers. With the extended time domain, we provide the chop modality with a non-overlapping interpretation. This allows some linear temporal operators explicitly dealing with the discrete dimension of time to be derivable from the chop modality in essentially the same way that their continuous-time counterparts are in the classical DC. This provides a nice embedding of some timed LTL (TLTL) modalities into DC to unify the methods from DC and LTL for real-time systems development: Requirements and high level design decisions are interval properties and are therefore specified and reasoned about in DC, while properties of an implementation, as well as the refinement relation between two implementations, are specified and verified compositionally and inductively in LTL. Implementation properties are related to requirement and design properties by rules for lifting LTL formulas to DC formulas.
Introduction
DC is born with a denotational approach [ZHR91], with which a system is modelled within a conventional
dynamic systems framework with states that are functions of time, the non-negative reals. When observing
a system, DC takes a continuous and global view: a property at a time point is observed through neighbourhoods
of that time point, and a Boolean state is observed through its duration in a bounded interval, i.e., the
integral of an indicator function. A property for an interval is specified by an arithmetical relation among
durations of states and real numbers.
This paper is to appear in Formal Aspects of Computing.
When specifying and reasoning about of requirements and high level designs for an embedded real-time
or hybrid systems[RRH93, ORS96, Liu96, REHR98], the dynamic systems model is beneficial because it
focuses on relevant observable states. Furthermore, the interval logic has simple interpretations in a timing
diagram for the states. The requirements will thus focus on sequencing of durational relations between
observable states rather than on sequencing individual state transitions. Properties of isolated time points
in the dense time domain are considered unobservable and ignored at the high level, therefore transitions
are only observed indirectly through the relation among states in the left and right neighbourhoods of the
transition point. A typical real-time property is the requirement of a bounded critical duration property,
that in every interval bounded by a length d the duration of a state P should not be more than c time units.
In DC this is nicely expressed as ' - d
However, when dealing with an implementation represented as a state machine such as an automaton or a
(abstract) program, it is a bit cumbersome in DC to apply structural induction over transitions. Also, at this
level of abstraction, stronger assumptions may be made about timing. For example, that a finite number of
state changes may occur simultaneously at a point of time, though in a specified order. Therefore, properties
at a real-time point becomes significant at this level, and it seems and advantage to change to a logic which
is focused on properties of transition sequences.
Linear Temporal Logic was introduced [Pnu77, MP81] for specifying and reasoning about reactive systems
modelled as transition systems [Kel76]. The properties of a transition system are qualitative safeness
(invariance) and responsiveness properties. While transition systems and (LTL) have been used successfully
for specification and verification of reactive systems, see e.g., [MP92], they are not expressive enough
for systems with real-time constraints which are bounded invariance and bounded responsiveness. Real-time
is introduced into transition systems either by associating lower and upper bounds on enabled transitions
[Lam77] or by introducing explicit clocks [AD90, AL92]. The first approach has led to extensions
of LTL with bounded operators [Koy89, AH90], and the second has used LTL with the explicit clocks
[PH88, AL92]. The relationship between the two approaches, that more or less one can be translated into
another, is investigated in [HMP94].
An advantage of the LTL frameworks is that transition systems are quite close to an implementation using
digital hardware and thus reflect semantics of programming languages. Another advantage is that invariance
properties and time bounded properties can be easily checked by structural induction over the transitions.
In some cases such properties may even be checked mechanically.
However, a system's behaviour is observed within these frameworks by looking into the state transitions
step by step. This approach is therefore inherently operational and less abstract than a dynamic systems
based framework. For instance, properties that relate states across several transitions have to be expressed
using auxiliary state variables - clock variables are a good example.
In general, a denotational approach reflects the engineering disciplines of requirement specification, system
design and verification, while an operational approach reflects the engineering disciplines of component de-
sign, refinement, and analysis. The contribution of this work is a feasible link between the two frameworks.
It is based on the preliminary results of [LRL98], but has a much simpler introduction of super-dense time,
trajectories, and LTL into the DC framework.

Overview

Section 2 presents a syntax, a semantics and an proof system of a combined logic. It extends the time
domain from the set of nonnegative reals R -0 to a two-dimensionaldomain R -0 \ThetaN. The second dimension
is discrete, the set of natural numbers N. The behaviour of a real-time system (i.e., a timed transition
systems) is defined as a set of functions, called trajectories, from this time domain to the pairs of states
of the system. We then extend the basic DC (i.e., the DC in [ZHR91]) by introducing actions (as in TLA
which describe state transitions.
The following sections show, how the logic is used to specify and reason about state properties and transitions
at a time point, and how it supports methods from both DC and LTL:
1. DC-style requirement and high level design specification and reasoning;
2. LTL-style operational and structural inductive proof methods for lower level properties;
3. Step-wise refinement from one implementation to another.
In particular, Section 3 recapitulates how the logic is used for DC-style specification and verification of high
level properties. Section 4 introduces timed transition systems (TTS) and their computations as trajectories,
and then Section 5 shows that the logic supports LTL-style specification of properties of a TTS. Section 6
recapitulates the structural induction rules from [HMP94] for timed transition systems; they remain valid in
the extended logic. The main contribution in Section 7 is to establish the relation between the specifications
of the two styles. Section 8 illustrates how the proof and refinement methodologies at the implementation
level within the TTS framework are linked to the DC methods used for the high level specification and
reasoning. Finally, Section 9 concludes with a discussion of the results.
2 The Logic
The logic is defined in terms of its syntax, semantics and proof system.
2.1 Syntax
As in the original DC [ZHR91], we consider the syntactic categories states, terms and formulas. Since we
also consider state transitions, we shall introduce the category of actions.
States: A state is the values that state variables of a dynamic system take at a moment of time. We use
for individual state variables, and \Pi is the set of all state variables.
A set of states is syntactically denoted by a predicate over state variables, values from their ranges, and
rigid (logical) variables, e.g., for state variables x ; y ranging over natural numbers,
are examples of states. We use for such state predicates. The set of
all state predicates is denoted State.
Actions: A state transition consists of a pair of states and is described by an action. It is a predicate over
the state variables and their primed versions x contained in the set \Pi 0 . Examples are x
unchanged over the changes to an arbitrary value), and x
and y change to sum and difference of the current values of x and y , respectively). We use -
actions.
Note that state predicates are a subset of actions - the actions which do not use any primed variables
Terms: Here, a term means an interval (or duration) term, rather than a term of state variables and
their values. For a given interval of time it denotes a real value. Thus the set Term of duration terms is
generated from durations R
, and is closed under real arithmetic operators. We
use to denote duration terms.
Formulas: As we shall describe duration properties for an interval as well as state changes at a time point
for an implementation, there are two kinds of elementary formulas: action formulas and duration formulas.
An action formula is simply denoted by an action, while a duration formula is a first order predicate over
duration terms. E.g; R
R
R
R
R
We use D to stand for an
elementary duration formula.
A general duration formula F is constructed from elementary formulas using the first order connectives and
the chop modality '; '.
For simplicity in this paper, we shall not use the logic to capture abstract liveness and fairness properties.
This would require the use of expanding modalities as found in [ZH96a, LRL97], and we choose to stay
with core Duration Calculus which is sufficient for the purpose of reasoning about safety and bounded
liveness properties.
2.2 Semantics
This subsection defines the semantics of the logic on the domain of trajectories.
Time: The time domain is Time def
N. For a position in Time, we denote p's
successor . Positions are ordered by the lexicographic ordering: ht 1
We also use the corresponding reflexive relation - def
For two positions p 1 and p 2 such that
the set of positions g. The set of all time intervals is denoted Intv .
Trajectories: Let \Sigma be the set of all possible mappings, from the state variables \Pi to their values
For a oe 2 \Sigma, and a X ' \Pi, oe[X ] denotes the values assigned to the variables.
A trajectory over \Sigma is a \Sigma. For a position p 2 Time, we use (ae 1 (p); ae 2 (p))
to denote the pair ae(p) which represents a state transition taking place at p. A trajectory ae must satisfy the
following conditions:
1. For each
2. ae is finitely variable, i.e., in a bounded time interval, [ha; mi; hb; ni], there is a finite number of of
state changes. This means that there exists a finite number of positions ht 1
that
(a)
(b) for each , the set fae 1 is a singleton.
In the usual model for LTL or TLA, a trajectory consists of singleton states. We duplicate the successor
state in the current state in order to use a non-overlapping definition of the chop operator.
For a trajectory ae over \Sigma, an observation over an interval [p consists of the pairs
g. In particular, at any real time point t , every observation over an interval [ht
finite non-empty sequence ae(t of state transitions.
States: For a trajectory ae, we define the value of a state predicate P at position p by
if P is false over ae 1 (p)
Terms: The meaning of a term ' under a trajectory ae is a real valued interval
We assume that the meaning of the function symbols: +, \Gamma, etc., are the associated functions of real
arithmetic. The meaning of a duration R
P is given by:
Thus, a duration ignores all the discontinuous positions, and its existence is guaranteed by the finite variability
of the trajectory. 1 The duration of the constant state true, i.e., R
true , denotes the length of the
and it is abbreviated as ' def
R
true .
Action Formulas: In Manna and Pnueli's LTL[MP92] or Lamport's Temporal Logic of Actions (TLA) [Lam94],
an action - (\Pi; \Pi 0 ) is interpreted over a state transition (oe; oe 0 ). It is true iff
When - is true of (oe; oe 0 ), it is called a -step. An action is then lifted up as a temporal formula being
interpreted over sequences of states.
In this paper, we lift an action - up to an interval formula: an action - is satisfied by a trajectory ae over an
observation if it holds at the first position of the observation
is true of
A state predicate P is a special action which does not refer to primed variables. The semantic definition
for an action implies that P holds for a trajectory ae over an observation if it holds at the first position of the
observation:
Each action - has an enabling condition which is a state predicate, denoted by en(-), and is true over a
state oe if there is state oe 0 such that (oe; oe 0 ) is a -step:
is the set of primed variables in - , which are treated as rigid variables in the above definition.
Duration Formulas: The meaning of a duration formula D is defined in terms of its satisfaction by a
trajectory ae and an interval [p denoted by ae; [p We assume the standard meaning of the
relational operators on reals. For example,
1 The logic is unchanged if
R
P is defined as
n)dt or as
General Formulas: We only present the semantics for the chop modality, while leaving the first order
connectives with their standard interpretation.
Given a trajectory ae and an interval [b; e], the formula F 1 ; F 2 is satisfied by ae over [b; e] iff there is a
middle position m such that b - m OE e, F 1 is satisfied by ae over [b; m] and F 2 is satisfied by ae over
This chop is not overlapping on the position m; therefore, a single position ht ; ki cannot be chopped.
A formula F is satisfied by a trajectory ae, written as ae holds for any interval [b; e]; F
is valid, written as it is satisfied by all ae over \Sigma.
Abbreviations: The following useful operators, some of which are from DC and LTL, can be defined
with the operators given above:
Almost everywhere
R
Hoare triple: fPg-fQg def
primed version of Q .
Somewhere: 3F def
The modality 3 is in ordinary DC expressed by the last subformula (true ; F ; true) only. However, the
presence of positions and the non-overlapping chop necessitate the three other cases.
2.3 Proof system
It is easy to see that in this logic, the validity of the axioms and rules in the first order predicate logic remain
valid for reasoning about action formulas. We now present axioms and rules for chop and duration.
Axioms for Chop From the its semantic definition, the chop operator is associative, distributive over -
and 9, and monotonic.
Axiom 2 If v is not free in F , then
Axiom 3 false ; F , false and F ; false , false.
Axiom 4 For any state predicate P ,
Rule
The soundness of a rule like Rule 1 means that the satisfaction of all the premises above the line by any
given ae implies the satisfaction of the conclusion under the line by the same ae. Therefore, we can infer the
validity of the conclusion from that of the premises.
Axioms for Durations The validity of all but one of the axioms and rules in the original DC for durations
is preserved in the semantics of this logic.
In the following, Axiom 6, Axiom 7, and Axiom 8 are the axioms in the original DC which remain valid
Axiom 9 is the original axiom R
R
R
positions
excluded; and Axiom 10 is new, introduced to characterize a point interval:
Axiom 6 R
Axiom 7 R
Axiom 8 R
R
R
R
R
R
R
fld e.
The above five axioms infer the super-dense property of the time domain: for any a - 0,
Also as expected, the finite variability ensures the soundness of the original DC induction rules:
Induction Rule I
If R(d e) holds, and (R(X -X ; dPe)-R(X -X ; d:Pe)) is provable from R(X ), then R(true)
holds.
Induction Rule II
If R(d e) holds, and (R(X -dPe is provable from R(X ), then R(true)
holds.
These rules can be used to prove the following theorems: for any state s
1. (true ; dPe) - (true ; d:Pe) - d e
2.
The finite variability assumption can be formalized as the following non-logical axioms, where P is any
state predicate.
Axiom
The relative completeness proof for durations found in [HZ97] should carry smoothly over for the new
logic. It seems also plausible that completeness results for the interval logic will be applicable.
3 Requirement and Design Specifications
The applications of DC to real-times systems in [ZHR91, RRH93, Rav95] show that when formulating
requirements to an actual system where we have decided on the relevant state variables, the procedure is
generally to identify safe or unsafe patterns of behaviour. The 'yardstick' properties when we consider
duration specifications are the following:
Bounded critical duration. The property P should not occur more than c time units within any time
window of T time units:
R
An important special case of this is the unbounded weak invariance property d e - dPe which is equivalent
to R
Bounded response. Every occurrence of P should be followed not later than after d time units by an
occurrence of Q .
A special case of this is (dPe equivalently dPe which asserts that P
never lasts for more than d time units.
Minimal separation. A property D cannot hold until P has been stable for at least l time units since the
change from a :P -state.
A specially useful case of minimal separation is that an occurrence of P following a :P must be stable for
at least d time units:
Often minimal separation is given by a formula dQe
and R ) :P . However, this can be deduced from the pure form using monotonicity, since dQe ; dPe ;
dRe implies d:Pe ; dPe ; d:Pe under the side conditions.
The bounded critical duration is related to the bounded response and minimal separation by the following
rule
Rule 3 dPe
Rule 3 is sound because the following implication can be proved
where D 1 and D 2 stand for the two premises, and C stands for the conclusion.
Gas Burner We now take the Gas Burner example in [RRH93, Lam93] to illustrate the requirement and
design specifications in DC. This case study formulates the safety requirement of a gas burner in terms of a
variable Leak denoting an undesirable but unavoidable state which represents the presence of unlit gas.
For safety, 'gas must never leak for more than 4 seconds in any period of at most 30 seconds'. This is
specified by the bounded critical duration property:
R
To meet the requirement Req , two design decisions are made:
Des 1
Des 2
Des
Des 1 is a bounded response property saying that any occurrence of Leak must be stopped within 4 seconds.
Des 2 is a minimal separation property saying that once a Leak is stopped it may not reoccur within 26
seconds. By Rule 3, we can derive the correctness of the design. i.e., any trajectory ae satisfying Des
satisfies Req .
Traditionally, Des is implemented by a real-time automaton or a real-time program P . Then the implementation
is described as a DC formula D(P), and the correctness of such an implementation is verified
by proving D(P) ) Des in DC. However, D(P) is in general a 'big' formula and the direct proof of
in DC is far from easy. We shall deal with this difficulty by adopting the compositional
induction proof techniques in the TTS framework.
4 Transition Systems
This section commences with an overview of untimed transition systems which are generally used as an abstract
model for reactive systems. Untimed transition systems are then extended to model real-time reactive
systems by imposing timing constraints on the transitions. Qualitative fairness requirements for transitions
are replaced by quantitative lower-bound and upper-bound real-time requirements. The exposition uses the
terminology of [HMP94]. However, trajectories are given in terms of a sequence of pairs, in order to be
consistent with the definition in the previous section.
4.1 Untimed transition systems
A transition system consists of four components:
1. \Pi is a finite set of state variables.
2. \Sigma is the set of state functions over \Pi.
3. \Theta is a state predicate, called the initial condition, that defines a subset of \Sigma called the initial states.
4. T is a finite set of state transitions (actions) over \Sigma. When a action - holds between states s and s 0
this is often written s -
A computation (execution, run) of a transition system S is an infinite sequence
which satisfies the following two conditions:
Initiation: oe 1
Consecution: For all i - 0, oe 2
stuttering step) or there is an action - in T
such that oe 1
diligent step).
Thus, a computation either contains infinitely many diligent steps, or it terminates with an infinite stuttering-
only suffix. The set [[S all computations of S is stuttering closed: if an infinite state sequence oe is a
computation of the program, then so is any state sequence obtained from oe by adding or deleting a finite
number of stuttering steps. Stuttering closure is the key to relate system specifications (or models) [AL91]
at different level of abstractions by refinement mappings.
4.2 Timed Transition Systems
We incorporate time in the transition system model by assuming that all transitions happen "instanta-
neously", while real-time constraints restrict the times at which transitions occur. The timing constraints
require transitions to be performed neither too early nor too late; for example, a valve controller should
not accept to be opened too quickly or be too slowly in closing. To describe such timing constraints, each
action - of a system is given a lower time bound l - , and an upper time bound u - . The lower time bound
is a value from R -0 and the upper time bound is either a value from R -0 or the special symbol 1, which
denotes the absence of an upper bound. Any real number in R -0 is assumed to be less than 1, and the
lower bound is assumed not to exceed the upper bound for any transition.
A timed transition system consists of an underlying transition system
and two functions l and u defining the transition time bounds for each transition.
A computation of is a trajectory over \Sigma which satisfies the following conditions.
1. Initiation: ae(h0; 0i) satisfies \Theta.
2. Consecution: For all position p, either ae 1 (p) or there is a - 2 T such that ae 1 (p) -
In the later case, we say that a - step is taken at position p of oe.
3. Timing constraints:
Lower bound: if - is taken at position p, there must exist a position p 1 - p such that d 1 (p;
and for any position p 2 , if is enabled at p 2 and - is not taken at position p 2 .
Upper bound: if - is enabled at position p, there exists
- is disabled at p 1 or - is taken at position p 1 .
A trajectory ae that satisfies the first two condition is a trajectory of the underlying transition system
traj be the set of all trajectories of the timed transition system S ; then it is easy to
prove that [[S is isomorphic to respect to the initial condition and transitions of S .
Let S be a transition system, a formula F is S -valid (or satisfied by S ), iff any trajectory ae 2 [[S
satisfies F . While a valid formula is S-valid for any given system S , the converse does not necessarily
hold. In fact a S-valid state assertion P may be falsified by some states of S which never occur in any
trajectory of S . To show that the given system S meets a specification F , it is enough to show that F is
S-valid. A proof rule is said S -sound if for any given TTS S , the S-validity of the premises implies the
S-validity of the conclusion. A sound rule, such as Rule 1 - Rule 3, is obviously S-sound.
A TTS model for the Gas Burner Intuitively, the design Des for the Gas Burner is modelled by a TTS,
GB 1 with only two states Leak and :Leak :
The problem is how to formally prove that this TTS satisfies Des and how to formally refine GB 1 .
5 LTL-Style Specification of Transition Systems
The 'yardstick' properties of a timed transition system include bounded invariance properties, and bounded
progress properties. These properties and the structural induction proof rules for them are given in [HMP94]
using timed linear temporal logic (TLTL). This section shows how these properties are incorporated into
the extended DC framework.
A state predicate P is an invariant of a transition system S if P holds at any position in any interval for
all trajectories of S . Thus, an unbounded invariance property is of the form 2P . P is an invariant of a
transition system S iff P is implied by \Theta, and P is preserved by all actions in T . Let fPgT fQg hold iff
T fPg-fQg holds for each - 2 T . An induction rule for proving an invariant of S is given in [MP81] as:
which is still S-sound in the interval logical setting, i.e., any transition system satisfying the premises also
satisfies the conclusion.
There are other induction rules for proving untimed properties which we leave out of this paper, because
we focus on the time bounded properties that are expressed by Duration formulas. As in [HMP94], we are
interested in proving bounded-invariance and bounded-response properties, and thus restrict ourselves to
the following bounded temporal formulas:
Primitive formulas: Actions are (linear) temporal formulas.
Boolean connectives: Every Boolean combination of temporal formulas is a temporal formula.
Bounded-eventually formulas: If OE is a temporal formula and u 2 R -0 , then 3 -u OE is a temporal formula;
it is true over a trajectory ae with an initial position ht there is a position ni such that
holds for the suffix of ae starting with p. We thus define
Bounded-unless formulas: If P is a state properties, OE is a temporal formula, and l 2 R -0 , then P U-l OE is
a temporal formula; it is true over a trajectory ae iff P holds at the initial position ht ae and either P
holds for all positions in ae, or there there is some position p such that t - holds for the suffix
starting with p, and P holds at every position q OE p. This formula can thus be defined as
We also denote P U-l true by 2 !l P when l ? 0, and define 2 !0 P to be true. In general we have for
any l 2 R -0 that 2 !l P ,
6 Induction Rules
In this section, we use the convention that the letters P , Q , R, as well as ', denote state formulas; - and its
indexed versions denote actions; OE, / and - stand for temporal formulas.
We start with bounded invariance properties. A bounded invariance property asserts that when some state
occurs a condition holds continuously for a certain amount of time. Such a property is specified by a
temporal formula of the form P Therefore, to prove a bounded invariance property, we often
have to prove a bounded unless property. There are five main rules for bounded unless in [HMP94] given
in

Table

1, which are still S-sound in our setting.
(R - OE)

Table

1: Rules for bounded unless
A bounded progress property asserts that once P occurs, Q must occur within a certain amount of time,
and thus is specified in the form P Again, the S-sound rules for bounded progress properties
in [HMP94] can be brought into our framework. They are given in Table 2.

Table

2: Rules for bounded progress
7 Linking rules
Now we are ready to provide the S - sound rules which link temporal properties to DC-invariance prop-
erties, DC-bounded response properties, and DC-minimal separation properties. The rules are presented
in the form such that the premises of a rule are temporal formulas (including first order predicates) and
the conclusion is an formula in DC. This indicates that a DC property can be derived from some TLTL
properties which can be verified by the structural induction rules.
The DC-invariance property d e - dPe is weaker than the temporal invariance property 2P :
A DC-bounded response property is of the form dPe asserting that P must be
followed within u time units by an occurrence of Q , and can be proved by the following linking rule:
A minimal separation property is described as a DC-formula of the form
which asserts that D cannot hold until :P has been stable for at least l time units since the change from
a P -state. Using bounded unless properties, we can prove a minimal separation property by the following
link:
OE
This rule is inductive in the sense that OE and / are temporal formulas which may be linked further to DC-
formulas. The first premise ensures the pattern (dPe ; (d:Pe ; OE)) does not collapse, the premise in the
second line says that a /-state sequence pattern can only proceed with P lasting for at least l 1 time units
followed by a :P -state and then a OE pattern, the premise in the third line then ensures that :P lasts for at
least l 2 time units.
The last two premises in the rule may be combined into one. However, the one in the second line have to be
established which then can be used to establish the last one by rule U -CSS. The special case when l
and / is dPe is often used. In this case the rule becomes
8 Implementation and Refinement of the Gas Burner
This section illustrates the linked methods in at development of the Gas Burner. We first show that the
timed transition system GB 1 given in Section 4 satisfies the specification Des in Section 3. Then we show
how GB 1 is refined into an implementation that may have only ignition failure. Finally, we present an
implementation of Des which tolerates both ignition and flame failures.
Theorem 1 The timed transition system GB 1 of Section 4 satisfies Des
Proof: Des 1 is deduced by Link-2 with the premises
Des 2 follows from Link-3 0 by T2 with l = 26. The proof is thus completed by the following Lemma 1. ~
Lemma 1 The time transition system GB 1 satisfies the following TLTL properties:
proven by applying 3 -SS to - 1
4, with the following
premises:
obviously valid in the untimed LTL proof system. (T 3 ) is established from (T 2 ) by applying U -
CSS for - 2 with l - 2
An implementation with ignition detection After the initial implementation, GB 1 can be refined in the
traditional TTS framework. For example, the transition system GB 2 in Figure 1 is a refinement of GB 1 .
GoIdle;
Idle
HeatOn;
Purge
Burn
FlOn

Figure

1: A refinement of GB 1
GB 2 has the following phases:
Idle: Await heat request with no gas and no ignition. It enters Purge within e time units on heat request.
The parameter e in this example is the system wide upper bound for reactions. 2
Purge: Pauses for seconds and then enters Ignite1 within e time units.
Ignite1: Turns on ignition and gas and after one second exits within e to Ignite2.
Ignite2: Monitors the flame, if it is sensed within one second Burn is entered, otherwise it returns to Idle
within e while turning the gas off.
In [RRH93, Lam93], a lower bound is also given. It is not needed for proving the correctness of this design.
Burn: Ignition is switched off, but gas is still on. The Burn phase is stable until heat request goes off.
Gas is then turned off and Idle is entered within e.
This refinement uses a simple error recovery: return to Idle from Ignite2. We assume no flame failure in
the Burn phase. Therefore, in this implementation, Leak can only occur in the Ignite1 and Ignite2 phases.
With the convention that the value of a variable x is changed by a transition - only if - names x 0 , the formal
definition of this refined transition system GB 2 is as follows.
\Theta def
(phase
(ignition
(ignition
GoIdle
The time bounds are given by Figure 1.
Let Leak 1 hold iff phase = Ignite1 holds and Leak 2 hold iff phase = Ignite2 holds. In the following, we
present the properties of these two leak states of GB 2 which correspond to the properties of Leak and have
the same proof routines as those for GB 1 .
Theorem 2 (GB 2 refines GB
. The timed transition system GB 2 satisfies
Proof: By 3 -SS with e, we can
establish
By 3 -SS with e, we can establish
By 3 -TRAN, (T 11 ) and (T 21 ) give us
obviously satisfied, and (T 3 ) can be established from
with a proof similar to the one for (T 3 ) in Lemma 1. ~
Using 22 ) for Leak 1 and Leak 2 , the following corollary can be proved in the
way that Theorem 1 is proved for Leak .
Corollary 1 The timed transition system GB 2 has the following properties if e - 1:
Property of GB 2 Property of GB 1
(Des
(Des
(Des
(Des 22
The proofs of Des 11 and Des 21 are the same as the proof of Des 1 of GB 1 , while the proofs of Des 12 and
Des 22 are the same as that of Des 2 for GB 1 , in Theorem 1.
Using the linking rules as in the proof of Theorem 1, Corollary 1 has the corollary below:
Corollary 2 The timed transition system GB 2 has the following properties if e - 1:
Property of GB 2 Property of GB 1
of Leak in GB 1
(Req
of Leak in GB 1
It is interesting to notice that Req of the Gas Burner (which is already deduced from Corollary 1 in Theorem
can be also deduced from Corollary 2 and the valid formula
R
R
R
An implementation with flame failure When the flame may disappear in the phase Burn, we can add
another simple error recovery procedure which enters Idle from Burn by switching off the gas. Formally,
we only have to redefine the action GoIdle in GB 2 as
GoIdle
Let Leak 3 denote (phase = Burn) - :Flame. The corresponding timed transition system GB 3 satisfies
Corollary 2 and the following property
(Req
which is of the same form as Req for the abstract state Leak in GB 1 and can be proved by the same proof
routine by which Req is proved for GB 1 .
Let Leak be the disjunction Leak 1 - Leak 2 - Leak 3 . By the valid formulas
R
R
R
R
R
this gives the following correctness theorem for
Theorem 3 (Correctness of GB 3 ) Assume that e - 2=3, the transition system GB 3 satisfies the requirement
Req of the Gas Burner system.
However, we should mention that GB 3 is not a refinement of GB 1 or GB 2 . It does not implement Des as
it does not meet Des 2 .
9 Conclusion and Discussion
This paper presents a logic which combine the original Duration Calculus approach in [ZHR91] and the
Linear Temporal Logic approach in [HMP94, Lam93] to specification and verification of embedded real-time
systems. The main idea is to use the DC for the specification of the system requirements and initial
design, and use the TTS for implementation and refinement. This combination provides both the advantage
of DC for directly modelling conventional dynamic systems with state that are functions of time, and
the advantage of TTS for modelling computation in reactive systems. Rules for linking the two level
specifications are given.
It is easy to see that the set of computations of a TTS in terms of trajectories is isomorphic to the set of
computations defined in [HMP94]. Within this framework, we can play the games in DC at a high level until
we obtain an initial design which corresponds to a simple TTS. Then we can refine this design totally within
the TTS framework, which supports formal verification of refinement between two TTSs [Lam94, AL91],
step by step until we obtain an implementation which can be coded into a program.
The approach is illustrated by solving the Gas Burner example. The advantage of the combined approach
becomes obvious if we compare with the solution in the single DC framework in [RRH93], and the solution
in the single TLTL framework in [Lam93]: specifications of the system at different levels are simpler and
better structured; the proofs of the correctness of the systems at different levels are easier as they directly
reflect the structural induction of each step in the refinement/implementation, and concrete states (e.g.,
at a lower level are reasoned about in the same way as the
corresponding abstract state (e.g., Leak in GB 1 ) at a higher level.
The combined logic allows us to describe multiple instantaneous transitions at a time point. For the same
purpose, Zhou and Hansen [ZH96b] and Xu [Xu97] introduce a dense-chop operator which can define
the meaning of the sequential composition of state transitions. The dense-chop operator is defined in different
computation models in these two papers. However, in both approaches the intermediate states of
a sequentially composite statement are hidden, and thus the semantics of x := is the
same as that of x := 3. This is a nice property if the approaches are used to deal with concurrent systems
with no shared variables. However, in shared memory based models such as TTSs, the semantics of
should be quite different from that of x := 3 k x := 0. The approach
in this paper defines DC in terms of trajectories of transition systems and define the satisfaction relation of
a duration formula by a transition system.
This paper has improved our earlier work in [LRL98] by redefining trajectories and the semantics of the
chop operator. This has allowed us to drop the notation for the step-counter variable, and to treat a state
predicate naturally as a special action.
Further work to this paper includes development of the full logic, perhaps based on the neighbourhood
modalities [ZH96a] which would provide a complete interval logic with extending modalities such that
abstract liveness and fairness properties can be treated. We do not foresee major changes by such an
extension. Another application would be to apply the linking techniques to the TLA-framework [Lam94];
ideally by putting the combined logic and its rules into one of the existing Duration Calculus Verification
assistants. Again, we do not see major technical problems in such a consolidation effort.



--R

Automata for modelling real-time systems

The existence of refinement mapping.

Temporal proof methodologies for timed transition systems.
Duration calculus: logical foundations.
Formal verification of parallel programs.
Specifying message passing and Time-critical systems with temporal logic
Proving the correctness of multiprocess programs.
Hybrid systems in TLA
The temporal logic of actions.
Specification and verification in the duration calculus.
Compositional inductive verification of duration properties of real-time systems
Verifying duration properties of timed transition systems.
The temporal framework for concurrent programs.
The Temporal Logic of Reactive and Concurrent Systems: Specifica- tion
Refining system requirements to program specifications.
Applications of temporal logic to the specification of real-time systems
The temporal logic of programs.
Design of embedded real-time computing systems
Engineering of real-time systems with an experiment in hybrid control
Specifying and verifying requirements of real-time systems
A semantics and verification of extended phase transition systems in duration cal- culus
An adequate first order interval logic.
Chopping a point.
A calculus of durations.
--TR
design;refinement;real-time;specification;verification