Timed Transition Systems* Thomas A. Henzinger Zohar Manna Amir Pnueli IR 92-1263 January1992 Department of Computer Science Cornell University Ithaca, NY 14853-7501 This research was supported in part by the National Science Foundation grants CCR-89-1 1512 and CCR-89-1 3641, by the Defense Advanced Research Projects Agency under contract N00039-84-C-021 1, by the United States Air Force Office of Scientific Research under contract AFOSR-90-0057 and by the European Community ESPRlT Basic Research Action Project 3096 (SPEC). Timed Transition Systems1 Thomas A. Heuzinger Computer Science Department Cornell University Ithaca, NY 14853 Zohar Manna Computer Science Department Stanford University Stanford, CA 94305 and Department of Applied Mathematics Weizmann Institute of Science Rehovot 76100, Israel Arnir Pnueli Department of Applied Mathematics Weizmann Institute of Science Rehovot 76100, Israel Abstract. We incorporate time into an interleaving model of concurrency. In timed transition systems, the qualitative fairness requirements of traditional transition system are replaced (and superseded) by quantitative lower-bound and upper-bound timing constraints on transitions. The purpose of this paper is to explore the scope of appli- cability for the abstract model of timed transition systems. We demonstrate that the model can represent a wide variety of phenomena that routinely occur in conjunction with the timed execution of concurrent processes. Our treatment covers both processes that are executed in parallel on separate processors and communicate either through shared variables or by message passing, and processes that time-share a limited number of processors under a given scheduling policy. Often it is this scheduling policy that determines if a system meets its real-time requirements. Thus we explicitly address such questions as time-outs, interrupts, static and dynamic priorities. This research was supported in part by the National Science Foundation grants CCR-89-11512 and CCR-89- 13641, by the Defense Advanced Research Projects Agency under contract N00039-84-C-o211, by the United States Air Force Office of Scientific Research under contract AFOSR-90-0057, and by the European Community ESPRIT Basic Research Action project 3096 (SPEC). 1 Introduction In [HMP9l], we extended the specification language of temporal logic and the corresponding ver- ification framework to prove timing properties of reactive systems. To model the timed execution of reactive systems, we generalized the computational model of transition systems conservatively by imposing timing requirements on the transitions. We claimed that a wide variety of real-time phenomena that are encountered in practice can be represented and analyzed within the model of timed transition systems. In this paper, we substantiate that claim. We use timed transition systems to model the timed execution of both multiprocessing and multiprogramming systems. Specifically, we address issues that routinely occur in real-time process communication, such as time-outs, and issues of real-time process control, including typical time-sharing strategies. By doing so, we enlargen the scope of applicability of the temporal proof methodologies for verifying timing properties of reactive systems that were presented in [HMP9l]. In our model, we assume a global, fictitious, real-valued clock, whose actions advance time by nonuniform amounts. The clock actions are interleaved with the system actions, which have no duration in time. In some other work aimed at the formal analysis of real-time systems, it has been claimed that while this interleaving model of computation may be adequate for the qualitative analysis of reactive systems, it is inappropriate for the real-time analysis of programs, and a more realistic model, such as maximal parallelism, is needed [KSdR+88]. One of the points that we demonstrate in this paper is a refutation of that claim. We show that by a careful incorporation of time into the interleaving model, we can still model adequately most of the phenomena that occur in the timed execution of programs. Yet we retain the important economic advantage of interleaving models, namely, that at any point only one transition can occur and has to be analyzed. We define the formal semantics of a real-time system as a set of timed execution sequences. This is done in two steps. First, in Section 2, we review the abstract computational model of timed transition systems and identify the possible timed execution sequences (computations) of any such system. Then, we consider concrete real-time systems and show how the concrete constructs can be interpreted within the abstract model. We begin, in Section 3, with the representation of real- time processes that are executed in parallel and communicate either through a shared memory or by message passing. Although the timeless interleaving of concurrent activities identifies true parallelism with (sequential) nondeterminism, when time is of the essence, we can no longer ignore the difference between multiprocessing, where each parallel task is executed on a separate machine, and multiprogrammin9, where several tasks reside on the same machine. This is because questions of priorities, interrupts, and scheduling of tasks may strongly influence the ability of a system to meet its timing constraints. These issues in modeling time-sharing systems are discussed in Section 4. 2 Timing Constraints for Transition Systems Timed transition systems generalize the basic computational model of transition systems [Kel76, Pnu77] by associating minimal and maximal time delays with the transitions. We use the real line as time domain and adapt the definition of timed transition systems that was given for a discrete time domain in [HMP91]. Similar notions of transition systems with timing constraints have been defined, for integer time, in [Har88, PH88, llMP9O, Ost90]. A transition system S = (V, ?, 0,7) consists of four components: 1. a finite set V of variables. 2 2. a set ? of states. Every state a E ? is an interpretation of V; that is, it assigns to every variable x E V a value a(x) in its domain. 3. a subset 0- c ? of initial states. 4. a finite set T of transitions, including the idle transition ri. Every transition r E T is a binary relation on ?; that is, it defines for every state a E ? a (possibly empty) set of r-successors --H(a) C ?. We say that the transition r is enabled on a state a iff r(a) # ?. In particular, the idle (stutter) transition ri = ?(Qa)ia??J is enabled on every state. All infinite sequence a = ....... of states is a computation (execution sequence, run) of the transition system 5 = (V, ?, 0-, T) iff it satisfies the following two requirements: Initiality a0 E 0. Consecution For all i> 0, there is a transition r E T such that Q+i E r(a?) (which is also denoted by a? Th Q+i). We say that the transition r is taken at position i of the computation a. We incorporate time into the transition system model by assuming that all transitions happen "instantaneously," while real-time constraints restrict the times at which transitions may occur. The timing constraints are classified into two categories: lower-bound and upper-bound requirements. They ensure that transitions occur neither too early nor too late, respectively. All of our time bounds are nonnegative integers N. The absence of a lower-bound requirement is modeled by a lower bound of 0; the absence of an upper-bound requirement, by an upper bound of 00. For notational convenience, we assume that oo _ n for all n E N. A timed transition system 5 = (V, ?, 0, T, 1, u? consists of an underlying transition system 5 --H (V, ?, 0,7) as well as 5. a minimal delay lT c N for every transition r E T. We require that lri = 0. 6. a maximal delay ?T E N u ?oo) for every transition - E T. We require that Ur > lr for all r E T, and that Ur = oo if r is enabled on any initial state in 0. In particular, Uri = 00. Let T0 C T be the set of transitions with the maximal delay 0. To allow time to progress, we put a restriction on these transitions. We require that there is no sequence To Ti Tn?1 a0 a1 ... ___ of states and transitions such that n > JT0J and rj E T0 for all 0 < i < n. This condition ensures the operationality (machine-closure) of timed transition systems [Hen9la]. Timed state sequences We model time by the real numbers R. A timed state sequence p = (a,T) consists of an infinite sequence a of states a? E ?, where i> 0 and an infinite sequence T of corresponding times Ti E R that satisfy the following two conditions: 3 Monotonicity For all i> 0 either Tj+1 = Ti, or Tj+1 > Tj and a?+I = that is, time never decreases. It may increase, by any amount, only between two consecutive states that are identical. The case that the time stays the same between two identical states is referred to as a stutter step; the case that the time increases is called a time step. Progress For all t E R, there is some i > 0 such that Tj > t; that is, time never converges. Since the time domain R contains no maximal element, there are infinitely many time steps in every timed state sequence. It follows that a timed state sequence alternates state activities with time activities. Throughout state activities, time does not advance; throughout time activities, the state does not change. Since all state activities are represented by finite subsequences, timed state sequences observe the condition of finite variability, namely, that the state changes only finitely often throughout any finite interval of time [BKP86]. A set II of timed state sequences is closed under stuttering iff (1) the sequence is in II precisely when the sequence is in II, and (2) the sequence --H+ (a?,T?) (oj,Tj) ... (Q",%') (ai,Ti+1) is in II precisely when the sequence ... (ai,Ti) (ai,t) (a?,T?+1) --H+ . is in II for Ti < t < Ti+i. To close a set of timed state sequences under stuttering, then, we must (1) add and delete finitely many stutter steps, and (2) spllt and merge finitely many time steps. Timed execution sequences Just as the execution sequences of transition systems are infinite state sequences, we model the execution sequences of timed transition systems by timed state sequences. The timed state sequence p = (a, T) is a computation of the timed transition system S = (V, ?, 0, T, 1, u) iff the state sequence a is a computation of the underlying transition system S- and Lower bound For every transition T E ? and all positions i> 0 and j > i with Tj < Ti + Ir, if r is taken at position j of a, then r is enabled on Q. In other words, once enabled, r is delayed for at least 17 time units; it can be taken only after being continuously enabled for l? time units. Any transition that is enabled initially, on the first state of a timed state sequence, can be taken immediately (as if it has been enabled forever). 4 Upper bound For every transition 7 E T and position i > 0 there is some position j > i with Tj < Ti + ?r such that either 7 is not enabled on or 7 is taken at position j of a. In other words, once enabled, ? is delayed for at most Ur time units; it cannot be continuously enabled for more than Ur time units without being taken. Since the maximal delay of every transition that is enabled initially must be 00, the first state change of a computation may occur at any time. Note that at both stutter steps and time steps, the idle transition ?I is taken. The idle transition marks phases of time activity throughout a computation; the other transitions are interleaved during phases of state activity. We consider all computations of a timed transition system to be infinite. Finite (terminating as well as deadlocking) computations are represented by infinite extensions that add only idle transitions; that is, a final, infinite phase of time activity. It is not difficult to check that the computations of any timed transition system 5 are closed (1) under stuttering and (2) under shifting the origin of time. The former property ensures that timed transition systems can be refined [Hen9ib]; the latter property means that timed transition systems cannot refer to absolute time. Specifically, the addition of a real constant to all times of a timed state sequence does not alter the property of being a computation of 5. Thus we will often assume, without loss of generality, that the time of the first state change of a computation is 0. Since the state component of any computation of 5 is a computation of the underlying untimed transition system 5--H, ordinary timeless reasoning is sound for timed transition systems: every untimed property of infinite state sequences that is satisfied by all computations of 5-, is also satisfied by all computations of 5. The converse, however, is generally not true. The timing constraints of 5 can be viewed as filters that prohibit certain possible behaviors of the untimed transition system 5--H. Special cases are a minimal delay 0 and a maximal delay oo for a transition 7. While the former does not rule out any computations of 5-, the latter adds to 5 a weak-fairness (justice) assumption in the sense of [MP89]: 7 cannot be continuously enabled without being taken. The choice of the real numbers as time domain is taken for the sake of concreteness. Indeed, any total ordering with an appropriate definition of addition by a unit (i.e., t < t + 1, and t < i' implies t + 1 < t' + 1) can be chosen as a time domain. In the case that the time domain is any one-element set, timed transition systems are easily seen to coincide with ordinary fair transition systems (with a weak-fairness requirement for every transition). 3 Modeling Time-critical Multiprocessing Systems The concrete real-time systems we consider first consist of a fixed number of sequential real-time programs that are executed in parallel, on separate processors, and communicate through a shared memory. We show how time-outs and real-time response can be programmed in this language. Then we add message passing primitives for process synchronization and communication. 3.1 Syntax: Timed transition diagrams A shared-variables multiprocessing system P has the form fol[P1l1 . . 11Pm]. 5 Each process Pi, for 1 < i < m is a sequential nondeterministic real-time program over the finite set Uj of private (local) data variables and the finite set U5 of shared data variables. The formula 0, called the data precondition of P, restricts the initial values of the variables in U = U5u ? Uj. 1 1: where the guard c is a boolean expression, x is a vector of variables, and e an equally typed vector of expressions (the guard true and the delay interval [0, co] are usually suppressed; for the empty vector nil, the instruction c nil := nil is abbreviated to c?). We require that every cycle in the graph consists of no fewer than two edges, at least one of which is labeled by a positive (nonzero) maximal delay. The intended operational meaning of the given edge is as follows. The minimal delay 1 guarantees that whenever the control of the process Pi has resided at the location for at least 1 time units during which the guard c has been continuously true, then Pi may proceed to the location ?k?. The maximal delay u ensures that whenever the control of the process Pi has resided at ?for tt time units during which the guard c has been continuously true, then Pi must proceed to ?kt (or, more precisely, time cannot advance before either the guard c becomes false, which may be caused by process parallel to Pi, or the process Pi proceeds). In doing so, the control of Pi moves to the location ik? "instantaneously," and the current values of e are assigned to the variables x. In general, a process may have to proceed via several edges all of whose guards have been continuously true for their corresponding maximal delays. In this case, any such edge is chosen nondeterministically. It follows that the control of a process Pj may remain at a location g forever only in one of two situations: if has no outgoing edges, we say that Pi has terminated; if each of the guards that are associated with the outgoing edges of the location is false infinitely often, we say that Pi has deadlocked. The second condition is necessary (although not sufficient) for stagnation, because if one guard is true forever, then the corresponding maximal delay u < oc guarantees the progress of Pi. 6 3.2 Semantics: Timed transition systems The operational view of timed transition diagrams can be captured by a simple translation into the abstract model of timed transition systems. With the given shared-variables multiprocessing system P: ?o1[P1II... 11Pm], we associate the following timed transition system Sp = (V, ?, 0, T, 1, u?: 1. V = Uu??,.. 7rmJ Each control variable ?i, where 1< i < m, ranges over the set LjUfIJ. The value of 7r? indicates the location of the control for the process P?; it is 1 (undefined) before the process Pi starts. 2. ? contains all interpretations of V. 3. 0 is the set of all states a E ? such that 0 is true in a and a(?) = 1 for all 1 < i < m. 4. T contains, in addition to the idle transition ri, an entry transition r0i for every process Pi, where 1 < i < m as well as a transition TE for every edge E in the timed transition diagrams for Pi,... Pm. In particular, a' E r?(a) iff = 1 and a'(r?) = 0i, = a(y) for all y E V --H firij. If connects the source location to the target location k? and is labeled by the instruction c := e? then a' E r?(a) iff = and a'(?) = c is true in a and a'(x) = = a(y) for all yE V --H 5. If r is an entry transition, then lT = 0. For every edge E labeled by the minimal delay 1, let lr? = 1. 6. If r is an entry transition, then Ur = 00. For every edge E labeled by the maximal delay tt, let Ur? = This translation defines the set of possible computations of the real-time system P as a set of timed state sequences. For instance, the computations of the trivial system P that consists of a single process with the timed transition diagram are exactly the timed state sequences that result from closing all sequences of the form (1,0) (o,O) (C0,t) (?1,t) (C1,1) (C1,2) where 0 < t < 1, under stuttering and shifting the origin of time. The condition on timed transition diagrams that every cycle contains at least one positive (nouzero) maximal delay ensures that the timed transition system Sp is operational. (The condition that every cycle contains at least 7 two edges guarantees that once a transition is taken, it cannot stay enabled, which simplifies the reasoning about timed transition systems [HMP9t].) We remark that our semantics of shared-variables multiprocessing systems is conservative over the untimed case. Suppose that the system P contains no delay labels (recall that, in this case, all minimal delays are 0 and all maximal delays are co). Then the state components of the computa- tions of Sp are precisely the legal execution sequences of P, as defined in the interleaving model of concurrency, that are weakly fair with respect to every transition [MP89]: no process can stop when one of its transitions is continuously enabled. Weak fairness for every individual transition and, consequently, progress for every process is guaranteed by the maximal delays 00. 3.3 Examples: Time-out and timely response We now model two typical real-time constructs as shared-variables multiprocessing systems to demonstrate the scope of the timed transition diagram language. In the first example (time-out), a process checks if an external event happens within a certain amount of time. In the second example (traffic light), a process reacts to an external event and is required to do so within a certain amount of time. A third example combines several processes. Time-out To see how a time-out situation can be programmed, consider the process P with the following timed transition diagram: true? We assume that the variable x ma?y be altered by some other process that is executed in parallel to P. When at the location C0, the process P attempts, for 10 time units, to proceed to the location Ci by checking the value of x. If the value of x is not found to be 0, then P does not succeed and proceeds to the alternative location C2 after 10 time units. The choice of the maximal delay u determines how often P checks the value of x. For example, if u > 10 then P may not check the value of x at all before timing out after 10 time units. If 0 < u < 10, then P has to check the value of x at least once every u time units. Consequently, if the value of x is 0 for more than u time units, it will be detected. On the other hand, the value of x being 0 may go undetected if it fluctuates too frequently, even in the case of u = 0. Traffic light To give another typical real-time application of embedded systems, let us design a traffic light controller that turns a pedestrian light green within 5 time units after a button is pushed. The environment is given by the following process E. Whenever the request button is pushed, the shared boolean variable request is set to true: 8 [0, 0] request true #Meo Recall that the edge labels true? and [0, oo] are suppressed; thus we have no knowledge about the frequency of requests. We wish to design a traffic light controller Q that controls the status of the traffic light through the variable light, whose value is either green or red. As unit of time we take the amount of time it takes to switch the light; for simplicity, we also assume that the time needed for local operations within Q is negligible. Now let us specify the desired process Q. The controller Q should behave in such a way that the combined system [request false, light redj [IIQ] satisfies the following two correctness conditions: (A) Whenever request is true, then light is green within 5 time units for at least 5 time units. (B) Whenever request has been false for 25 time units, then light is red. The first condition, (A), ensures that no pedestrian has to wait for more than 5 time units to cross the road and is given another 5 time units to do so. The second condition, (B), prevents the light from being green indefinitely (under the assumption that any controller Q resets the variable request to false whenever it is read and found to be true). It is not hard to convince ourselves that, once it is started, the following process Q satisfies the specification: ?request _ [6,6] [0,0] request request :--H false [0, 0] request := false light := green for any delay 4 < 6 < 23. This implementation of the traffic light controller turns the light green as soon as possible after a request is received and then waits for 6 time units before turning the light red again. If the request button has been pushed in the meantime, the light stays green for another 6 time units. Multiple traffic lights We now generalize the traffic light example and design a system that reacts to several external events. We wish to do so by composing, in paraliel, processes that are similar to Q. At this point it is convenient to accept some additional assumptions about the frequencies of the external events. In our example, we suppose that the distance between any two requests is at least 15 time units; that is, 9 [1,1] light green request true Under this assumption, we can simplify the traffic light controller to request false [0, 0] for ally delay 4 < ? < 17. The combined system : ?request false, light = redj [E'(tQ'] still satisfies both correctness requirements (A) and (B). Now consider a more complex traffic light configuration, with two lights and two request buttons. In particular, we assume that the second light is designed for the spedal convenience of pedestrians in a hurry: it is required to turn green within 3 time units of a request but, on the other hand, has to stay green for only 3 time units. While pedestrians arrive at the first light with a frequency of at most one pedestrian every 15 time units, we assume that the more urgent requests are less frequent at most one every 30 time units: i: #&??[0?0] request1 := true E?: $Mi?[o?o] request2 := true The controller for both lights executes the following two processes: l0 Qi: request1 request1 :=false [0,0] tight1 := red [1,1] Th p1 [1,1] light1 := green light2 := red [1,1] request2 :=false [0,0] t2 [1,1] MW' light2 := green If the combined traffic light controller makes use of two processors and the processes Qi and Q2 are executed in a truly concurrent fashion, then the correctness of the entire system : frequest1 request2 false, light1 light2 = red] [111E211Q111Q2] follows from the correctness of its parts. Specifically, if 4 s < 17 and 2 < 62 < 23, then all runs of P satisfy the following conditions: (A1) Whenever request1 is true, then light1 is green within 5 time units for 5 time units. (A2) Whenever request2 is true, then light2 is green within 3 time units for 3 time units. (B1) Whenever request1 has been false for 25 time units, then light1 is red. (B2) Whenever request2 has been false for 25 time units, then light2 is red. A more interesting case is obtained if only a single processor is available to control both lights and the two processes Qi and Q2 have to share it. Using the interleaving (shuffle) operator of [Hoa85], we denote the resulting system by the expression P111: frequest1 = request2 =false, light1 = light2 = red] [iII211(QiiIIQ2)]. Note that the behavior of the environment E111E2 is still truly concurrent to the behavior of the traffic light controller Q1111Q2, which executes both processes Qi and Q2 on a single processor in an interleaved fashion. Let us assume that 6i = 10 and 62 = 2, a case in which the multiprocessing P\i is correct. However, if we have no knowledge about the strategy by which the processes Qi and Q2 are scheduled 011 the processor they share, other than that it is fair (i.e., the turn of each process will come eventually), then the time-sharing system P?j does not satisfy the specification consisting of the requirements (A1), (A2), (B1), and (B2). This is easy to see. Suppose that the process Qi is, for some time, given priority over the process Q2, and the traffic light controller receives a request for the second light only 1 time unit after it has received a request for the first light. Then it will serve the first request by turning light1 green and (busy) waiting for 10 time units, thus violating (A2). On the 11 other hand, if the process Q2 that serves the more urgent yet less frequent requests is always given priority over the process Qi, then the system Pjj is correct. This is because of the low frequency of requests for the second light only one such request can interrupt the service of a request for the first light. Before we discuss the modeling of time-sharing, priorities, and interrupts in greater detail, let us first stay with truly concurrent processes and introduce message-passing operations. 3.4 Message passing Asynchronous message passing can be modeled by shared variables that represent message channels. In this subsection, we extend our timed transition diagram language by a primitive for synchronous (CSP-style) message passing, which can be used for the synchronization and communication of parallel processes. Syntax A (message-passing) multiprocessing system P has the form f?J[P1ll . . 11Pm], where 0 is a data precondition and each process Pi, for 1 < i < m, is a sequential nondeterministic real-time program over the finite set Uj U U8 of data variables (in the case of pure message-passing systems, U5 = ?). We employ again timed transition diagrams to represent processes, but enrich the repertoire of instructions by guarded send and receive operations. The send operation a!e outputs the value of the expression e on the channel a. The receive operation a?x reads an input value from the channel a and assigns it to the variable x. A send instruction and a receive instruction match iff they belong to different processes and address the same channel: For any two matching communication instructions with the delay intervals [1, u] and [1', tt,], respec- tively, we require that max(l, i') < min(u, tt'). Since we use the paradigm of synchronous message passing, a send operation can be executed only jointly with a matching receive operation. Thus the intended operational meaning of the given two edges is as follows. Suppose that, for max(l, 1') time units, the control of the process Pj has resided at the location C? and the control of the process Pj' has resided at the location and the guards c and c' have been continuously true. Then Pj and Pjt may proceed, synchronously, to the locations 2k and ?,, respectively. On the other hand, if Pi has resided at e,i. and pi' has resided at e3ii, and the guards c and c' have been continuously true for min(u, u') time units, then both processes must proceed. In doing so, the current value of e is assigned to x. 12 Semantics Synchronous message passing can be modeled formally by timed transition systems. We define the timed transition system Sp = (V, ?, e, T, 1, u? that is associated with the given message- passing multiprocessing system P as in the shared-variables case, only that T contains an additional transition for every matching pair of communication instructions. Suppose that the two edges E (from 4 to Ctk) and E' (from 41, to Ck?',) in the timed transition diagrams for Pi and Pji are labeled by the matching instructions c e!o and c' a?x, respectively. Then o+ T contains, for the matching edges E and E', a transition rE?EI such that a' E r?,?t(a) iff = 4. and a'(r?) = = 41, and a'(r?i) = c and c' are true in a and a'(x) = = a(y) for all YE V --H fri,rjt,xJ. o+ If the matching edges and ` are labeled by the minimal delays 1 and 1', respectively, let 1?E,E' = max(1,1'). o+ If the matching edges and E' are labeled by the maximal delays u and n', respectively, let UTEEI = min(tt,u'). This translation defines the set of possible computations of any distributed real-time system P whose processes communicate either through shared variables or by message passing. Process synchronization Recall that the component processes of the multiprocessing system P1j?P2 may start at arbitrary, even vastly different, times. An important appllcation of synchronous message passing is the syn- chronization of parallel processes. Let P1 and P2 be two real-time processes whose timed transition diagrams have the entry locations ? and o2, respectively, and let a be a channel. Now consider the two processes P1 and P2 whose timed transition diagrams are obtained from the transition diagrams for P1 and P2 by adding new entry locations: P1: [0,0] 0 P2: [0,0] 0 The added message-passing operations have the effect of synchronizing the start of the two processes P1 and P2 (whenever message passing is used for the purpose of process synchronization only, the data that is passed between processes is immaterial and the data components of the send and receive instructions are usually suppressed). It follows that the component processes of the multiprocessing system P1iP2 start synchronously, at the exact same (arbitrary) time. From now on, we shall write P1??,P2 for the system P whose component processes P1 and P2 start synchronously; that is, the notation P1 iisP2 is an abbreviation for the message-passing system P1 liP2. Equivalently, we can directly define the formal semantics Sp of the synchronous multipro- cessing system P1J?8P2 as containing a single entry transition rJ'2 for both processes Pi and P2; namely, a' E r?'2(a) iff 13 = a(?2) = I, = ? and a'(r2) --H = a(y) for all yE V --H ?r1,r2J. It is not hard to generalize our notion of synchronous message passing to synchronous broadcasting, which allows arbitrarily many parallel processes to synchronize simultaneously on joint transitions. 4 Modeling Time-critical Multiprogramming Systems While the interleaving model for concurrency identifies true parallelism (multiprocessing) with nondeterminism (multiprogramming), the traffic light example of the previous section suggests that the ability of a system to meet its real-time constraints depends crucially on the number of processors that are available and on the process allocation algorithm. This dependence is already vividly demonstrated by the following trivial system consisting of the two processes pi and P2: If both processes are executed in parallel on two processors, we denote the resulting system by pi lip2 (or Pi JI8P2, if the processes are started at the same time); if they share a single processor and are executed one transition at a time according to some scheduling strategy, the composite system is denoted by Pill P2. In the untimed case, it is the very essence of the interleaving semantics to identify both systems with the same set of possible (interleaved) execution sequences the stuttering closure of the two state sequences (?0i,e02) ? (4,o2) ? (4,?) (?oi,?o2) ff42 (?oi,?) ff4 (4,4) ,` ... (a state is an interpretation of the two control variables irj and 7r2). Real time, however, can distinguish between true concurrency and sequential nondeterminism: if both processes start syn- chronously, then the parallel execution of p1 and P2 terminates within 1 time unit; on the other hand, any interleaved sequential execution of P1 and p2 takes 2 time units. This distinction must be captured by our model: 1. In the two-processor case p1 ??8p2, we obtain as computations the timed state sequences that result from closing the two sequences (1,1,0) (0i,02,0) (?0i,02,1) ff4 (4,e02,i) ff4 (4,i2,1) (4,4,2) (1,1,0) (?0i,?02,0) (0i,02,1) ff4 (?0i,4,1) ff4 (4,i2,l) (4,4,2) under stuttering and shifting the origin of time (the third component of every triple denotes the time). The system p1 ??p2 has more computations, because the time difference between the start of P1 and the start of p2 can be arbitrarily large. 14 2. In the time-sharing case P1 lIP2, the set of computations will be defined to be essentially the closure of the two timed state sequences (1,0) (01,e02,o) (o1,?o2,1) ? (1i,?o2,1) (4,#o2,2) ? (4,?2i,2) (1,0) (C01,t02,o) (?o1,?o2,1) ??2 (e01,?,1) (?o1,?2i,2) ? (4,2i,2) under stuttering and shifting the origin of time. We write "essentially," because we will augment the states by information about the status of the two processes (either active or suspended). Also, observe that we have silently assumed that the swapping of processes is instantaneous and that neither process has priority over the other process. All of these issues will be discussed in detail. Thus, for modeling time-critical applications, we can no longer ignore the difference between mul- tiprocessing and multiprogramming. In this section, we first show how our model extends to concrete real-time systems that consist of a fixed number of sequential programs that are executed, by time-sharing, on a single processor. Then we use our framework to represent general, distributed multiprogramming systems, in which several processes share a pool of processors statically or dy- namically. 4.1 Syntax and semantics A multiprogramming system P has the form toJ[P1111 . . 111Pm]. Each process Pj, for 1 < i < m is again a sequential nondeterministic real-time program over the finite set U of data variables, whose initial values satisfy the data precondition 0. We represent the real-time programs Pi by timed transition diagrams as before. Note, however, that in the multiprogramming case the control of the (single) processor resides at one particular location of one particular process. Thus the intended operational meaning of the edge 4. ffi is as follows. The minimal delay 1 guarantees that whenever the control (of the single processor) has resided at the location j? for at least 1 time units and the guard c is true, then the control may proceed to the location ?kt. The maximal delay u ensures that whenever the control has resided at for n time units and the guard c is true, then it must proceed to tk. This is because, in the single-processor case, no other process can interfere with the active process and change the value of c. The operational view of the concrete model is again captured formally by a translation into timed transition systems. With the given multiprogramming system P, we associate the following timed transition system Sp = (V, ?, 0, T, 1, u): 1. V = Uu??,?1,... 7rm). There are two kinds of control variables: the processor control variable ? ranges over the set .1.... m, IJ; each process control variable 7rj, for 1 < i < m ranges over the set Li of locations of the process Pi. The value of the processor control variable ? is I (undefined) before the (single) processor starts executing processes. Thereafter the control 15 of the processor resides at the location r? of the process P?. We say that the process P? is active, while all other processes Pj, for i $ `t, are suspended (if the value of ? is undefined, then all processes are suspended). The process control variable 7rj of a suspended process indicates the location at which the execution of Pj will resume when Pj (re)gains control of the processor. 2. ? contains all interpretations of V. 3. e is the set of all states a E ? such that 0 is true in a, and a(?) = I, and a(r?) = e0? for all 1