BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR94-1436
ENTRY:: 1994-08-26
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Hybrid Verification by Exploiting the Environment
AUTHOR:: Fix, Limor 
AUTHOR:: Schneider, Fred B. 
DATE:: July 1994
PAGES:: 16
ABSTRACT::
A method of verifying hybrid systems is given. Such systems involve state 
components whose values are changed by continuous (physical) processes. The 
verification method is based on proving that only those executions that 
satisfy constraints imposed by an environment also satisfy the property of 
interest. A suitably expressive logic then allows the environment to model 
state components that are changed by physical processes.
END:: CORNELLCS//TR94-1436
BODY::
Hybrid Verification by Exploiting the
Environment*
Limor Fixt
Fred B. Schneider
TR 94-1436
July1994
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
*Work supported in part by the Office of Naval Research under contract N00014-
91-J-1219, The National Science Foundation under Grant No. CCR-9003440,
DARPNNSF Grant No. CCR-9014363, NASNDARPA grant NAG-2-893, and AFOSR
grant F49620-94-1-0198. Any opinions, findings, and conclusions or
recommendations expressed in this publication are those of the author and do not
reflect the views of these agencies.
tLimor Fix is also supported, in part, by a Fullbright post-doctoral award.
Hybrid Verification by Exploiting the Environment*
Limor Fixt			Fred B. Schneider
Department of Computer Science
Cornell University
Ithaca, New York 14853
June 30, 1994
Abstract. A method for verifying hybrid systems is given. Such systems involve state
components whose values are changed by continuous (physical) processes. The verifi-
cation method is based on proving that only those executions that satisfy constraints
imposed by an environment also satisfy the property of interest. A suitably expres-
sive logic then allows the environment to model state components that are changed by
physical processes.
1 Introduction
What executions of a concurrent program are possible and what properties are satisfied by that
program may depend on the environment. Consider a system to maintain a given water level in
a tank. Under computer control, a pump causes water to be added and a valve causes water to
be drained. Correctness of the control program depends on the environment--Hin particular, on
the rate at which the pump adds water and the rate at which the valve drains water. In fact,
correctness of the control program is defined in terms of permissible states of the environment,
because correctness is based on the water-level. 0ne simply cannot specify or reason about such a
control program without saying something about its environment.
In (10] we introduced two principles for verifying programs whose executions are affected by an
environment. The state of the environments considered in [10] change discretely aiong with each
atomic action of the program. Nevertheless, our principles were shown to be usable for verifying
real-time behavior of concurrent programs, because schedulers and resource limitations that affect
execution time can be regarded as part of the environment. In this paper, we extend those results
to environments having variables that change value continuously, as time passes. The result is a
new verification method for hybrid systems.
The remainder of this paper is structured as follows. In Section 2, we review the principles
introduced ill [10]. Section 3 presents a simple concurrent programming language, giving a plausible
semantics for programs that will control physical processes. 0ur specification language is discussed
in Section 4. Section 5 explains how invariancebased proof methods for verifying safety properties
*Work supported in part by the Office of Naval Research under contract N0001?9l-J-1219, the National Science
Foundation under Grant No. CCR-9003440, DARPA/NSF Grant No. CCR-9014363, NASA/DARPA grant NAG-2-
893, and AFOSR grant F49620-94-1-0198. Any opinions, findings, and conclusions or recommendations expressed in
this publication are those of the author and do not reflect the views of these agencies.
tLimor Fix is also supported, in part, by a Fullbright post-doctoral award.
can be used for verifying hybrid systems as well. Section 6 contains an example. And, Section 7
puts our work in context. A soundness proof of our verification method appears in an appendix.
2 Formalizing and Exploiting the Environment
Any method for program verification comprises: a programming language, a property language,
and a way to prove that a program P satisfies a property ?. Program P and the property ?
define sets [[Pj] and [[?]] of behaviors, where a behavior is a mathematical object that describes an
execution of the program. A program P satisfies a property ?, denoted (P, ?) E Sat, exactly when
all behaviors of P are permitted by ?:
E Sat if and only if [[P)] c [[?]]
The environment in which a program executes defines a property too. This property contains
behaviors that are not precluded by one or another aspect of the environment. For example, with
the water tank discussed above, the environment defines a property containing those behaviors
where the water level changes continuously and only by amounts consistent with the pump's rate
and the valve's rate. Behaviors in which the water level changes abruptly are not in this property.
For a property g defined by an environment, the feasibie behaviors of a program P under C are
those behaviors of P that are also in C: [[Pi] n ([C]]. A program P satisfies a property ? under an
environment g, denoted (P, g, ?) E ESat, if and only if every feasible behavior of P under ? is in
(P, g, ?) E ESat if and only if ([[P]] n [[?j]) c [[?]]
Based on simple set theory and (1), we also have
(P, ?, ?) E ESat if and only if [[P]] c ([[?j] u [[g]]),
where [[?]] denotes the set complement of [[?]].
3 Programs
(1)
(2)
Consider a simple programming language having an empty statement (skip), assignment (:=),
sequential composition (;),iteration (do), and parallel composition (I I). To simplify the exposition,
we assume that every program is a parallel composition of exactly two sequential processes. The
syntax of a program P is given by the following grammar:
P:: 511152
5:: skipl:=e 5i;5? I doGi?5i[]...[]Gn?5n0d
The skip statement does not change any program variable; some non-zero time elapses.
Assignment r := e changes variable x to be the same value as expression e. The value of e is
computed at some instant after execution of the assignment is started; x is changed instantaneously
after some additional time elapses. Thus, execution of our assignment involves performing two
atomic actions.
Sequential composition Si; 52 is executed by first executing Si and if and when Si terminates,
52 is executed.
Execution of a do statement 5 involves repeating the following until no longer possible: use
guard evaluation action Gvals to evaluate Boolean guards ..... . , Gn and select a corresponding
2
Si:
II
52:
do PS = off A WL < 50			ps := on
B PS = on A WL> 95 off
[] ?(ps = off A WL < 50) A ?(ps = on A WL > 95) skip
od
do vs = close A PRESSED vs 0Pefl
vs = o?en A PRESSED vs close
B ?PRE5SED?skip
od
Figure 1: Program P
statement S? whose guard is true. Then, execute 5?. Thus, once none of the guards evaluates to
true, the do terminates. Execution of Gvals is not instantaneous but uses values of variables that
are all read together some time after Gvals starts; the statement selection occurs some time after
these values have been read.
Finally, execution of a parallel composition Si II 52 results in the simultaneous execution of Si
and 52. It terminates once both Si and 52 have terminated.
Program Semantics using Control-Graphs
We represent a program using a control graph a collection of nodes and edges, not unlike a
flowchart. Each node models a delay prior to executing an atomic action; each edge models exe-
cution of an atomic action and describes a state change that occurs (instantaneously). Thus, skip
gives rise to a single node followed by a single edge, whereas an assignment x := e gives rise to a
sequence of two nodes one whose outgoing edge computes the value of e and a successor whose
outgoing edge updates x.
Formally, a controlgraph is a tuple (V, E, Ventr?, Ec?it), where:
o+ V is a set of nodes.
E is a set of edges. Each edge (v, V') is labeled with a Boolean expression g and a multiple
assignment 0P (possibly empty, i.e., skip). When convenient, we denote such a labeled edge
by the 4-tuple (v, v', 9, oP). We call v the source node of the edge and call v' the destination
node. Destination node v' must be either an element of V or the distinguished node "?".
o+ Ventry is a set of entry nodes. Ven?r,, ? V
o+ Eexit is a set of exit edges, those edges with "?" as their destination node. Ecrit c E.
As an example, consider sequential subprogram Si of Figure 1. The control graph of Si is given
in Figure 2. We use double circles to indicate entry nodes, and each edge is labeled with a Boolean
expression and an assignment.1 The Boolean expression labeling an edge must hold in order for that
edge to be traversed; the assignment is executed whenever the edge is traversed. Thus, in Figure
2, node v0 is the sole entry node and allows the passage of time before Gval51 reads variables Ps
and WL. The edge from v0 to Vi, labeled with no guard and assignment t1, t2 := PS, WL, models
1When the guard is omitted, ?fru? is intended; when the assignment is omitted,?kip" is intended.
3
pa
Figure 2: Control graph of Si
that read. Edges from v1 model the actual selection (and exit from the loop). The edge from v1
to v2 is labeled with Boolean expression t1 = off A t2 < 50 to signify that assignment ps := on is
selected for execution only if the values read for PS and WL satisfy PS = off A WL < 50. Nodes v2
and v3 model assignment ps := on; v4 and v5 model assignment ps := off; and v6 models the skip.
Appendix A gives a procedure for translating a program into a control graph. When that proce-
dure is used, the control graph CGp for any program P: 511152 contains exactly two disconnected
subgraphs, each with a single entry node: one entry node is for subprogram Si and the other is for
subprogram 52.
States, Phases, and ?aces
A state is a mapping from variables to values. The variables are partitioned into program variables,
environment variables, control variables, and clock variables. Progium variables (which are typeset
using lower-case identifiers) appear in assignments, as targets and/or expressions. Execution is the
only way to change program variables. In the program of Figure 1, ps and vs are examples of
program variables.
Environment variables may appear in guards and the expressions of assignments but may not
appear as targets of assignments. We typeset environment variables using upper-case identifiers,
to distinguish them from program variables. Environment variables are presumed to be changed
by the environment, perhaps based on physical or chemical processes governed by scientific laws.
In Figure 1, WL and PRESSED are environment variables.
For verification, it is useful to associate with each node v of the control graph a Boolean control
variable v. The value of control variable v is true if and only if an atomic action modeled by an
4
edge from node v can next be executed. If control variable v is true, then we say that node v is
active.
Finally, clock variables capture elapsed time since various control graph nodes were last active.
Clock variable now records the elapsed time since the program started execution. Clock variable
Iv contains the elapsed time since control variable v last changed from false to true and has value
1 if v has never become true. Thus, Iv contains the elapsed time since node v last became active.
And, clock variable lv contains the elapsed time since the start of control variable's v last change
from true to false; it has value I if v has never been true.
Execution of a program is modeled as a sequence of phases [18, 12]. Each phase gives values
to the variables over some period of time. ?Ve denote a phase as a pair ([r,r'], f), where [r,r'] is
a closed interval of the reals and f is a mapping from [r,r'] to states. Phase ([r,r'],f) associates
state f(t) with any time t such that r < t < r'.
A trace r is a possibly infinite sequence of phases
([ri, r'i], fi), ([r?, r?'], f2),
(3)
such that for all i, r: = r?+1. The length Iri of a trace r is defined to be infinity if there are infinite
number of phases in the trace and otherwise is T?1 of its last phase ([r?, T'n], f?). A length m prefix,
with r? < m < r??, of r,denoted by r..m, is a finite trace
([ri, r'i], fi), ([T2, r?'], f2), . , ([r?, m], fi).
Notice that a trace associates two states with the endpoints of each phase.2 This is because we
intend execution of an atomic action to delimit adjacent phases. State f?(r11) occurs just prior to
executing the atomic action that terminates phase ([ri,r?'i,fi); state f?+i(r?+i) is the one produced
by executing that atomic action.
Trace r of (3) is a behavior of a program P, hence an element of [[P]], provided all state changes
are consistent with execution of P. For this to be so, first we require of initial phase ([r1,r'1],f1):
o+ r1 = 0.
o+ now = 0 in state fi(ri).
o+ Exactly the two control variables that correspond to the entry nodes of the control graph for
P are true in state fi(ri).
o+ If a control variable v is true in state f1(r1) then clock variable Iv equals 0 in that state.
Otherwise tv equals I in state f1(r1).
o+ For all control variables v, lv equals I in state fi(ri).
Second, we require that no program variable or control variable x changes value during a phase.
(Environment variables and clock variables are not so constrained.)
(Vj.rj < j < r'? : fj(j)(x) = fj(rj)(x))
Third, we require that for any adjacent phases
2There are two exceptions. Only a single state is associated with the very beginning of the trace; and for finite
traces, only a single state is associated with the very end of the trace.
5
differences between states fi(r?') and f?+1(r?+i) are the result of executing a single atomic action.
That is, the state change can be attributed to traversing an edge e in the control graph where (i) the
source node is active, (ii) the guard evaluates to true in state f?(r'?), and (iii) any changed program
variables in state f?+1(r?+1) are the result of executing the multiple assignment labeling edge e.
Our control graphs are for 2-process programs, so without loss of generality, let control variables v
and v, be true in phase (fri,r?'],fi), control variables v' and w be true in phase (ki+i,r?'+1],f?+i),
and edge (v, v', g,x := ?e) be in the control graph.3 We formalize requirements (i) through (iii) by:
Exactly two control variables are true in each of states f?(r1') and f?+1(r?+1), and one of those
control variables is true in both f?(r?') and j?+i(r?+i). This corresponds to the restriction that
only a single process executes a single atomic action between adjacent phases.
o+ Guard y is true in state fj(r??). This means that edge (v, v', y,op) can be traversed.
The value of every program variable of x in state f?-+i(r?+i) is equal to the value of the
corresponding expression in e in state fi(r?'); the value of no other program variable and no
environment variables changes between f?(r1,) and f?+1(r?+1). Thus, state changes are due to
executing assignment  :=
o+ Clock variable Iv' equals 0 in state f?+j(r?+1); clock variable and tv equals 0 in state f?(4).
This causes the clock variables to have their intended meanings.
Finally, all clock variables change value within a phase ([ri, r;j, f?) in the expected way. The
value of a clock variable c at time t, where t satisfies r? < t < T?j? is given by
fi(t)(c) = fj(ri)(c) + (t --H
A clock variable c that is not reset in state fj(r?') also satisfies fi(r?')(c) = f?(r?)(c) + (r?' --H
The following diagram summarizes how the starting and ending states of adjacent phases in a
trace are related. A dashed arrow indicates changes to environment and clock variables; a solid
arrow denotes changes to program variables, control variables, and clock variables that occur by
traversing a control graph edge. The trace begins at state fi(O) and the state changes continuously
according to the function fi, until time r'1. At time ??1, an instantaneous state change occurs
corresponding to execution of some atomic action. This causes the state to change from fi (r'1) to
f2(r2), based on the assignment labeling the edge of the control graph that is traversed and the
resetting of certain clock variables.
J1(o)
!i(ri')
---- ? !2fr2,)
\I
J3(r3) -- - --H?
3If z and e are empty, then the effect of execution is the same as skip.
6
4 Properties
We now introduce a language for expressing properties. We restrict consideration to safety prop-
erties [15], properties that assert some "bad thing" does not happen during execution. Informally,
formula Init ? El defines the property containing all traces r such that (i) Init does not hold
initially on T or (ii) I holds throughout r. Thus, I implies that the "bad thing" being prescribed
by the safety property has not happened.
In formula Init ? El, we call Init and I assertions and assume that they are defined by the
grammar below. There, we assume x is a program variable, X is an environment variable, and v
is a control variable. We also assume a set C of real constants. Finally, 0Pret denotes a relational
operator and 0Parith an arithmetic operator.
A :: T OPret T' ?A A A A' (Vx.A : A')
T			::			C			Var			Tdt(Var) jT OParith T' T(T'? fTT? T"
Var			::			x			X v			Iv 1 lv I now
(4)
For any variable a, term Tdt (a) is the first derivative of a with respect to time. The past term
T(T'? equals the value of T at the (past) state existing T' units ago. And, ITT' T11 is the value of
the definite integral of term T" between T and T'.
We formalize the value MT(T) of a term T in a finite trace r inductively.
MT(C)(T) =
MT( Var)(r) =
MT(?dt(Var))(T) =
c
f?(r1,-)( Var), where ([r?, r?'1, f?) is the last phase in r
lim?r????T(Var)(r)?M?(Var)(Tiri???)
(5)
MT(T Oparith T')(r) = M?(T)(r) OParith MT(T')(T)
=			MT(T)(T..JrI?MT(T')(r))
MT(fT' T")(r) =			fMM;($T\k(T)) MT(T11)(T..t)dt
The value MA(A) of an assertion A in finite trace r is a Boolean function defined in the usual way
using MT.
An assertion A is defined to be valid iff for every finite trace T, MA(A)(T) = true. We assume
a deductive system is available for proving validity of assertions.
Finally, we formalize the set of traces in [[Init ? El]]. It is just those finite and infinite traces
T for which M?(Init)(r,.o) = false or, for all j, MA(I)(T..j) = true:
r E [[Init ? El]] : M?(Init)(r..o) = false or
(Vj.O < j < IT : AlA(I)(r..d) = true)
5 Verifying Hybrid Systems
(6)
When verifying a hybrid system, we are interested in proving that executions of a program P
satisfy [[Init ? El]] if environment variables change values according to some given constraints
(presumably dictated by scientific laws). In the parlance of Section 2, this is an instance of proving
that P satisfies [[Init ? El]] under an environment g, where C is the property asserting that
environment variables only change values according to the given constraints.
7
Define the hybrid-environment property E Env, for Env an assertion, to be the set of all finite
and infinite traces where Env holds throughout:
T E [[EEnv]] : (Vj.O <j < tri : ?%4?(Fnv)(r.j) = true) (7)
Hybrid-system verification is thus equivalent to establishing_(P, EEnv, Init ? El) E ESat. Accord-
ing to (2), it suffices to prove [[P]] c ([[Init ? El]] u [[EEnv]]). ?Ve accomplish this by introducing
another property [[It]], called a hybrid proof outline, satisfying:
c--H			[[It]]			(8)
[[It]] c ([[Init ? El]] U [[EEnv]]) (9)
A hybrid proof outline, like an ordinary proof outline, associates assertions with control points.
In particular, a hybrid proof outline associates an assertion with each node in a control graph.
Assertions are of a restricted form so they cannot be invalidated by changes to environment variables
(which might occur while a given node of a control graph remains active).
Ri:
Clock variables c and environment variables X appear only in past terms having the form
X(c?. Such terms do not change value during a phase, even as clock variables advance and
the environment variables are updated.
R2: Terms using derivatives are not permitted.
Formally, a hybrid proof outline is a triple It = (CGp, ?, Env) where CGp is a control graph
for a program P, ? maps each node v among the nodes V of CGp to an assertion ?? satisfying Ri
and R2, and EEnv is a hybrid-environment property. The assertion
:			A v ?			(10)
vEV
is called the invariant of It. Property [[It]] is defined to be the set of all finite and infinite traces
r such that (i) r does not satisfy hybrid-environment property EEnv or (ii) r E [[Ii< ?
For an assertion A, we write A[ := e] to denote the textual substitution of every free occurrence
of x in A by e. The following theorems give conditions for verifying_(8) and (9) above, and therefore
they give a method for establishing [[P]] c ([[Init ? El]] U [[EEnv]]).
Theorem 1 Given a hybrid proof outline It = ((V, E,Ventr?, Eexit),?, Env) for program P, then
c [[It]] if the following conditions hold:
o+ For every (v,u,g,op) E E:
(Env A v A ?? A gA ?v = 0) ? (u A ??)[op, In := 0,v := false, u := true]
is valid.
o+ For every (v, u, g, op) E  and every w E V such that v and w are nodes of different processes:
(Env A VA ? A g A wA ?wA Iv = 0) ? (w A ?w)[op, In := 0,v := false, u := true]
is valid.
Theorem 2 Given a hybrid proof outline It = ((V,E,Ventr?,Eexit),?, Env), if
and (EnvAI?)?l
(Env A Init) ?
are valid, then [[It]] c ([[Init ? El]] U [[EEnv]]).
The proofs of both theorems are in Appendix B.
8
1 = ciose A m2 = tr?e
w6
6 Example
Figure 3: The control graph of 52
vs open
To illustrate the approach, we return to the control program in Figure 1. Sub-program Si reads
the water level (WL) in a tank. If the level is too low--Hless than or equal to 50--Hthen a pump
is activated, causing water to be added, until the level reaches 95. Sub-program 52 monitors a
control button. When the button is pressed, 52 toggles the valve state. The two components for
the control graph of this program appear in Figures 2 and 3.
A hybnd?environment property EEnv for this system asserts that changes to the water level
are based on the pump rate and valve state. We assume a pump with throughput 0.5 ?/sec and a
valve that passes 0.25 /sec. When the valve is closed and the pump is off the water-level does not
change:
(ps = off A vs = close) ? ?ddt(wL) = 0
When the valve is open and the pump is on, the water-level increases at the rate of 0.25 ?/sec,
reflecting the relative capacities of the valve and pump:
d
(ps = on A vs = open) ? dt? WL) = 0.25
When the valve is open but the the pump is off, the water-level decreases at the rate --H0.25 ?/sec:
d
(ps = off A vs = open) ? dt ? WL) = --H0.25
9
Finally, when the valve is closed and the pump is on, the water-level increases at the rate of 0.5
(ps = onA vs = close) ? ?ddt(?VL) = 0.5
The water level changes over time. This is reflected by the following assertion, which states
that while any control variable u holds, the water-level equals whatever it was when u first became
true plus the change to the water-level since that time:
A			WL = WL(Tu? + f?o)iu ft(WL)
uE4vov6,wo,...w6?
We assume that execution of each program step takes at least 0.5 units of time and at most 1
unit of time:
(n?(Iu<--H 1))A((tu=0)?(Itt>?O.S))
A
tE?vov6,w?),...w6)
Notice that real-time execution bounds are defined using an assertion about the environment. This
seems natural, since there is nothing intrinsic about the program text that supplies such bounds.
Rather, the bounds are an artifact of the particular processor executing the program. Moreover,
associating the bounds with the environment makes it possible to use our verification framework
for different real-time behaviors.
The property that we wish to establish is that our control program ensures that the water-level
remains between 48 and 98. We formalize this property as Init ? CI, where:
Init: PS = off A vs = close A vo A wo A ?PRES5ED A WL(Ivo? = 90
I: 48 < WL < 98
To prove that this property holds, we construct a hybrid proof outline ?, with the following
mapping ? that assigns an assertion to every node in the control graph. Let ? denote the xorlogic
operation.
(v0 ... .? v6)A (wo ?. . e w6) for i = O..6
?v0 :(vs = open v vs = close)A
(ps = onv PS = off)A
PS = on ? 48.5 < WL(Iv0? < 96A
PS = off ? 49.5 < WL(Iv0? < 98
?v1 (vs = open V VS = close)A
(ps = onVPS = off)A
ps = on ? 48.75 < WL(Ivi? < 96.5A
Ps = off ? 49.25 < WL(Ivi? < 98A
t1 = ps A t2 = WL(Ivi?
?v2 (vs = open V vs = close) A PS = offA
49 < WL(Iv2? < 50
?V3 (vs = open V VS = close)A ps = offA
48.75 < WL(Iv3? < 50
?v4 (vs = open V VS = close) A PS = onA
95.25 < WL(Iv4? < 97
10
?v5 :(vs = open V vs = close) A ps = onA
95.5 < WL(Iv5? < 97.5
?v6 :(vs = open V vS = ciose)A
(ps = on V ps = off)A
ps = on ? 49 < WL(Iv6? < 95.5
PS = off ? 49.75 < ?VL(Tv6? < 96.5
According to Theorems 1 and 2, we must then check the set of verification conditions listed in
Appendix C.
7 Discussion
Our work is perhaps closest in spirit to the various approaches for reasoning about open systems. An
open system is one that interacts with its environment through shared memory or communication.
The execution of such a system is commonly modeled as an interleaving of steps by the system and
steps by the environment. Since an open system is not expected to function properly in an arbitrary
environment, its specification typically will contain explicit assumptions about the environment.
Such specifications are called assume-guarantee specifications, because they guarantee behavior
when the environment satisfies some assumptions. Logics for verifying safety properties of assume-
guarantee specifications are discussed in [9, 14, 21]; liveness properties are treated in [1, 3, 23]; and
model-checking techniques based on assume-guarantee specifications are introduced in [6, 11].
Our approach differs from this open systems work both in the role played by the environment
and in how state changes are made by the environment. We use the environment to represent
aspects of the computation model and the scientific laws governing the behavior of environment
variables--Hnot as an abstraction of the behaviors for other agents that will run concurrently with the
system. This generalizes what is advocated in [8] for reasoning about fair computations in temporal
logic. Second, in our approach, every state change obeys constraints defined by the environment,
while in the open systems view only state changes that are attributed to the environment must
obey those constraints.
Interest in verification of hybrid systems is an outgrowth of work in verifying real-time bounds
for concurrent programs. A rather substantial literature exists on the subject; see [7] for a collection
of surveys. The problem of reasoning about arbitrary continuous-valued state components was first
discussed in [24], in connection with process control program for railroad control. That work was
ultimately published in [20].
Our underlying semantic model--Htraces--His similar to the hybrid traces of [18]. A hybrid trace
consists of continuous and discrete moments. A continuous moment is mapped to a single state, and
a discrete moment may be mapped to several states. With our notion of traces, every intermediate
discrete moment is mapped to exactly two states.
Our computation model control graphs and hybrid-environment properties share features
with phase transition systems [18, 12], hybrid statecharts [19], and hybrid automata [2]. Our
computation model differs in its separation of program execution from changes to the environment.
The control graph models program execution and the hybrid-environment property models state
changes to the continuous-valued variables. One advantage of this separation is that changes to
the computation model and to the physical laws can be easily accommodated. A second advantage
is that assertions associated with control points in a program (i.e., nodes in the control graph) can
be simpler because they need not explicitly mention environment state components.
11
Our specification language contains constructs for derivatives and integrals. Such constructs also
appear in the specification languages of [4, 12, 17, 5, 22]. Our verification methodology extends the
Hoare-logic methodology of [16] to hybrid system. Deductive-systems for proving safety properties
of hybrid system are also presented in [19, 13]. Our work differs mainly in its independence from
a particular computation model.
References
[1]
M. Abadi and L. Lamport. An old-fashioned recipe for real-time. In J.W. de Bakker, W.-P.
de Roever, and G. Rozenberg, editors, Real-time: Theory in Practice, pages 1-17. Lecture
Notes in Computer Science Vol. 600, Springer-Verlag, 1992.
[2] R. Alur, C. Courcoubetis, T.A. Henzinger, and P-H. Ho. Hybrid automata: An algorithmic
approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode,
A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 209-229. Lecture Notes in Computer
Science Vol. 736, Springer-Verlag, 1993.
[3] H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications.
In 16th Annual ACM Aymposium on Theory of Computing, pages 51-63, 1984.
[4] Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing
Letters, 40(5):269--H276, 1991.
[5]
Z. Chaochen, A.P. Ravn, and M.R. Hansen. An extended duration calculus for hybrid real-time
systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems,
pages 36--H59. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.
[6] E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proceedings
4th IFEE Symposium on Logic in Computer Science, pages 353--H362, 1989.
[7] J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg (eds.). Real-Time: Theory
in Practice. Lecture Notes in Computer Science Vol. 600, Springer-Verlag, 1992.
[8] E.A. Emerson. Alternative semantics for temporal logics. Theoretical computer science, 26:121--H
130, 1983.
[9] L. Fix, N. Francez, and O. Grumberg. Program composition via unification. In 19th Interna-
tional Colloquium On Automata, Languages and Programming, pages 672-684. Lecture Notes
in Computer Science Vol. 623, Springer-Verlag, 1992.
[10] L. Fix and F.B. Schneider. Reasoning about programs by exploiting the environment. To
appear, 21st International Colloquium On Automata, Languages and Programming.
[11]
0. Grumberg and D.E. Long. Model checking and modular verification. In CONCUR `91, 2nd
International Conference on Concurrency Theory, pages 250--H263. Lecture Notes in Computer
Science Vol. 527, Springer-Verlag, 1991.
T.A. Henzinger, Z. Manna, and A. Pnueli. Towards refining temporal specifications into hybrid
systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems,
pages 60--H76. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.
12
[12]
[13]
J. Hooman. A compositional approach to the design of hybrid systems. In R.L. Grossman,
A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 121--H148. Lecture Notes
in Computer Science Vol. 736, Springer-Verlag, 1993.
[14] C.B. Jones. Specification and design of (parallel) programs. In R.E.A. Mason, editor, infor-
mation Processing `83, pages 321--H332. Elsevier Science Publishers, 1983.
[15] L. Lamport. Proving the correct ness of multiprocess programs. lEEF Trans. Software Engi-
neering, 3:125--H143, 1977.
[16] L. Lamport. The hoare logic ofconcurrent programs. Acta Informatica, 14, 1980.
[17] L. Lamport. Hybrid systems in tla+. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel,
editors, Hybrid Systems, pages 77-102. Lecture Notes in Computer Science Vol. 736, Springer-
Verlag, 1993.
[18]
[19]
[20]
0. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J.W. de Bakker,
C. Huizing, W.-P. de Roever, and G. Rozenberg, editors, REX Workshop, Real-time: Theory
in practice, pages 447--H484. Lecture Notes in Computer Science Vol. 600, Springer-Verlag, 1992.
Z. Manna and A. Pnueli. Verifying hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn,
and H. Rischel, editors, Hybrid Systems, pages 4--H35. Lecture Notes in Computer Science Vol.
736, Springer-Verlag, 1993.
K. Marzullo, F.B. Schneider, and N. Budhiraja. Derivation of sequential real-time, process-
control programs. In A. Van Tilborg and G. Koob, editors, Foundations of Real-Time Com-
puting, pages 39--H54. Kluwer Academic Publishers, 1991.
[21] J. Misra and M. Chandy. Proofs of networks of processes. IEEE Transactions on Software
Engineering, SE-7(4):417--H426, 1981.
[22] X. Nicollin, J. Sifakis, and 5. Yovine. From atp to timed graphs and hybrid systems. In
J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg, editors, REX Workshop,
Real-time: Theory in practice, pages 549--H572. Lecture Notes in Computer Science Vol. 600,
Springer-Verlag, 1992.
[23] A. Pnueli. In transition from global to modular temporal reasoning about program. In K.R.
Apt, editor, Logics and models of concurrent systems, pages 123--H144. NATO ASI Series, Vol.
F13, Springer-Verlag, 1985.
[24]
F.B. Schneider. Designing real-time systems (that really work!). Invited lecture at Symposium
on Formal Techniques in Real-Time and Fault-Tolerant Systems, Warwick, England, Sept.
1988.
A Constructing a Control Graph
The control graph CG5 that corresponds to a sub-program 5 is defined inductively, as follows:
o+ For 5 a skip: Define V = fvo?, Ven?y = [vo), E = [eoj where eo = (v0,?,true,skip), and
Eexit =
13
o+ For 5 an assignment x := e(?):4 Define V = ?v0,v1?, Ventry = (v0?, and E = (eo,e1Y where
e0 = (v0,v1,true,t := ?y), e1 = (v1,?,tru?,x := e(t)), and Eexit =
o+ For 5 a statement composition Si; 5?: Let (V', E1, ??ntry' Ec1eit) be the control graph for Si
and let (V2, E2, Ve2ntry, Ee%it) be the control graph for 52. Define V = V' UV2, Ventry = V'ntry?
Eexit = ??tt, and
0
0
E = E1 u E2 --H Ee'xit U ((v, v', g, op) ?(v,?,g,op) E Ee1xit and v' E Ve2ntry)
For 5 an iteration do C1 5, BC2 52 od:5 Let y be the list of variables mentioned by Ci
and C2. Let (V1,E1, Ve1ntry, Ee'xit) be the control graph for Si and let (V2, E2, V2ntry, Ee2xit)
be the control graph for 52. Define V --H V' uV2 U (v0, v,), Ventry = (v0),
E' U E2 --H Ec1eit --H Ee2eitU
((v0,v1,true,t :=
(vi,v,CiFt/,skip) v E Ve1ntry) U (v,,v,C2[?,skip) v E Ve2ntry)U
((v,,?, ?C,(?t/y] A ?C2[t/?], skip))U
((v, v0, g, op) ?(v,?,y,op) E Ec1eit U Ec2eit)
and Eceit = ((vo,?, ?CiFt/?y] A ?C2Ft/?y], skip))
For 5 a parallel composition Sill 5?: Let (V1,E1, Vt'ntry' Ee'eit) be the control graph for Si
and let (V2, E2, Ve2ntry, Ee2eit) be the control graph for 52. Define V --H V' U V2, Ventry --H
Ve1ntry UVe2ntry, Eeet? = Ee'xit U Ee2eit? and E --H E1 U E2.
B Soundness Proofs
Lemma 1 Let A be an assertion satisfying Rt and R2, and let T be a finite trace. If r' is a finite
trace, r is a prefix of r1, and
(Vj.lrl <j < l?l : r% (x) --H r(x) for every program variable x, and
= r(y) + j --H l?l for every clock variable y),
then Yj.lrl <j < Ir' : MA(A)(T) =
Proof: Since A satisfies Ri and R2, it refers only to program variables and to past terms of
the form z(y?, such that z is an environment variable and y is a clock variable. Therefore, the
evaluations of the terms of A at T and at ft? return that same values.
Theorem 1 Given a hybrid proof outline TL = ((V,E,Ventry, Eextt),?, Env) for program P, then
c [(?]] if the following conditions hold:
o+ For every (v,u,g,op) E E:
(Env A vA ?? A gA lv = 0) ? (n A ?u)[op, I? := O,v := false,n := true]
is valid.
4e(??) denotes that expression e refers to variables in list y.
5To simplify the presentation, we assume only two alternatives.
14
o+ For every (v,u,g,op) E E and every w E V such that v and ware nodes of different processes:
(Env A VA ? A g A wA ?wA iv = 0) ? (w A ?w)[op, In 0, v := false, u true]
is valid.
Proof:
1. Let T E [[P]], where T = (fri,r'1],fi),(fr?,r21],f?),...
2. According to definition of [[It]] we need to prove that either, (i) r ? [[?Env]], or (ii)
MA(I?)(r..o) = false, or (iii) (Vj.O < j < Iri : MA(I?)(T.J) = true). It therefore suf-
fices to prove that if (i) and (ii) do not hold then (iii) holds.
3. Assume (i) and (ii) of 2 do not hold, sorE [[EEnv]] and M?(I?)(r..o) = true.
4. By induction on the number i of the phases in r, we next prove:
(Vj.O <j < r : MA(I?)(r.4) = true)
Basis: i = 1. According to 3 we have that MA(I?)(T..o) = true. According to 1 and Lemma
1 we conclude (Vj.O < j < r1, : ??A(I?)(T.3) = true).
Step: Assume (Vj.O < j < r;?1 : ?`4A(1?)(7..j) = true) holds for i > 1. We prove:
(Vj.ri <j < r1, : ?\4A(J?)(T.4) = true)
(a) MA(Env A I?)(r_r'_ ? = frue, by the step assumption and 3.
(b) Without lose of generality, assume (vi?i,wi?i) ? (vi,wi) such that vi?1 ? Vj? Wj?1 =
Wj? and vi?i and Wi--Hi are true in According to 1, 4(a), and the definition of I?:
MA(EnV A Vi?i A wt-?i A ???? A ???-? A gA Ivi?i = O)(r_r'_ ? = true
(c) Let r? be obtained by extending r?r:?i with the single phase ([ri, ri], fi). Then, according
to the hypotheses of the theorem and 4(b)
MA(Vi A Wj A ???- A ?Wt )(r*) = true
(d) Let j be such that r? < r?'. Then since r E [[P]], according to 1 and due to Lemma
1:
MA(Vi A Wi A ? A ?wi)(T*) = MA(Vi A Wi A ?? A ?wt)(T..?)
(e) According to 4(c), 4(d) and definition (10) of I?, MA(I?)(T4) = true.
Theorem 2 Given a hybrid proof outline It = ((V, E, Ventr?, eit), ?, Env), if
(EnvAThit)?I? and (EnvAI?)?I
are valid, then [[It]] c ([[Init ? El]] u [[EEnv]]).
Proof:
15
1. Let r E [[Ii]].
2. According to definition of [[Tt]], either:
(a) T E [[EEnv]]. In this case, T ? ([[Inft ? EJ]] u [[EEnv]]).
r E [[CEnv]] and MA(I?)(T..0) = false. In this case, since (Env A Init) ? l? we
know MA(Env A i??it)(r..o) = false. However, since M?(Env)(r..o) = true we get
MA(Init)(r..0) = false. Therefore according to definition (6), 7 E [[Init ? cl]] and
thus 7 E ([[Init ? cl]] u [[EEnv]]).
7 E [[EEnv]] and (Vj.O < j < 171: ???(Env A l?)(7..j) = true). In this case, since
by hypothesis (Env A l?) ? 1 we get (Vj.O < j < 171:__J'4A(1)(7.j) = true). Thus,
7 E [[Init ? El]] and this implies 7 E ([[Init ? cl]] u [[cEnv]]).
C The verffication conditions
The following conditions must be proved valid in ordered to complete the verification. To use
Theorem 2, we must prove:
o+ (EnvAi??it)?l?
o+ (EnvAI?)?l
For Theorem 1, we must prove:
o+ (Env A V0A ??A ivo = 0) ? (v1 A ??1 )[t1,t2 := PS, ?VL, Tvi := O,v0 := false, vi := true]
o+ (Env A v1 A ??? A t1 = off A t2 < 50A tv? = 0) ? (v2 A ?v2)[Iv2 := 0, v1 :=false, v2 := true]
o+ (Env A v1 A ??? At1 = on At2 > 95A Ivi = 0) ? (v4 A ?4)[Iv4 := O,v1 := false,v4 := true]
o+ (EnvAv1A??1 A(?(t1 = off At2 < 50)A?(t1 = on At2> 95))A ivi =0) ? (v6A?v6)[IV6
0, v1 := false, v6 := true]
o+ (Env A v2A ???A iv2 = 0) ? (v3 A ?v3)[IV3 := O,v2 := false, v3 := true]
o+ (Env A V4A ?v4A ?V4 = 0) ? (v? A ?v?)[?vs := O,v4 := false, v5 := true]
o+ (Env A v6 A ?v6A 1v6 = 0) ? (vo A ?vo)[Ivo := 0,v6 := false, vo := true]
o+ (Fnv A v3 A ??A 1v3 = 0) ? (v0 A ???)\j)s := on, Tvo := 0,v3 := false, v0 := true]
o+ (Env A v5A ?v5A ivs = 0) ? (v0 A ?vo)[p5 := off, Tvo := 0,v5 := false,vo := true]
o+ (EnvAwiAgA Iwi = 0) ? (w,)[op, jw3 := 0,Wj := false,w? := true] for every (w?,w?,g,op) E
o+ (Env A v A ? A 9 A WA iv = 0) ? (w)[op, Iu := 0,v := false,u := true] for win CGs2 and
(v,u,g,op) in CGs,
o+ (Env A w A Ag A vA ?vA 1w = 0) ? (v A ?v)[oTh Iu := 0,w := false, u := true] for v in CGs1
and (w,u,g,op) in CGs2.
16
