Composition and Refinement of Discrete Real-Time Systems Jonathan S. Ostroff Department Of Computer Science, York University, 4700 Keele Street, North York Ontario, Canada, M3J 1P3. Email: jonathan@cs.yorku.ca    Tel: 416-736-2100 X77882   Fax: 416-736-5872. Abstract: Reactive systems exhibit ongoing, possibly non-terminating, interaction with the environment. Real-time systems are reactive systems that must satisfy quantitative tim- ing constraints. This paper presents a structured compositional design method for discrete real-time systems that can be used to combat the combinatorial explosion of states in the verification of large systems. A composition rule describes how the correctness of the sys- tem can be determined from the correctness of its modules, without knowledge of their internal structure. The advantage of compositional verification is clear. Each module is both simpler and smaller than the system itself. Composition requires the use of both model-checking and deductive techniques. A refinement rule guarantees that specifications of high-level modules are preserved by their implementations. The StateTime toolset is used to automate parts of compositional designs using a combination of model-checking and simulation. The design method is illustrated using a reactor shutdown system that can- not be verified using the StateTime toolset (due to the combinatorial explosion of states) without compositional reasoning. The reactor example also illustrates the use of the refine- ment rule. Keywords: Real-time reactive systems, formal methods tools, statecharts, temporal logic, modules, abstraction, refinement, composition, model checking. Table of Contents 1.0 Introduction 3 2.0 Background 6 2.1 Real Time Temporal Logic (RTTL) 6 2.2 Timed Transition Models (TTMs) 8 2.3 Parallel composition of TTMs 12 2.4 Overview of the StateTime toolset 12 3.0 Modules and module composition 15 3.1 Parallel composition of modules 16 3.2 Modes of interface variables 19 3.3 A small example of compositional reasoning 20 4.0 Module refinement 23 4.1 Observation equivalence of TTMs 23 4.2 Observation equivalence of modules 27 5.0 Modular Design of the delay reactor trip (DRT) 28 5.1 Informal description of the problem 28 5.2 Formal requirements 30 5.3 Problem to be solved 33 5.4 Controller design 34 5.5 Refining the controller 36 5.6 The design method 38 6.0 Conclusions and related work 39 7.0 References 42 Figure FIGURE 1. Structure diagram for compositional design method 5 FIGURE 2. Plant module 14 FIGURE 3. The relay module 20 FIGURE 4. Module for majority voting logic 21 FIGURE 5. Observably equivalent TTMs 24 FIGURE 6. Analog implementation of the delay relay trip timing. 29 FIGURE 7. The observable inputs and outputs of the DRT 30 FIGURE 8. Architecture of the controller based on majority voting control 32 FIGURE 9. Structure diagram for the DRT 34 FIGURE 10. Control module 35 FIGURE 11. Refinement of microprocessor control module 37 1.0 Introduction Reactive systems exhibit ongoing, possibly non-terminating, interaction with the envi- ronment. Real-time systems are reactive systems that must satisfy quantitative timing con- straints. This paper presents a structured compositional design method for discrete real- time systems that can be used to combat the combinatorial explosion of states in the verifi- cation of large systems. A system is decomposed into parallel components called modules. A composition rule describes how the correctness of the system can be determined from the correctness of its modules, without knowledge of their interior structure. The advantage of compositional verification is clear. Each module is both simpler and smaller than the system itself. In addition to system decomposition, an abstract specification of a module may need to be refined into implementations closer to code. A refinement rule guarantees that specifi- cations of abstract modules are preserved by their implementations. The StateTime toolset is used to automate parts of compositional designs using a com- bination of model-checking and simulation. The design method is illustrated using a reac- tor shutdown system that involves the use of three microprocessors, each independently checking sensor readings, with the final decision to shut down based on a majority vote. The single microprocessor version can be checked in the StateTime toolset without com- positional reasoning. However, the three-microprocessor system suffers from a combina- torial explosion of states and a compositional approach is thus needed. The reactor example also illustrates the use of the refinement rule. The compositional design method is based on the TTM/RTTL framework [36,37,40] which consists of the following: € A constructive description language called timed transition models (TTMs) for describing reactive systems. A TTM is a guarded transition system with lower and upper time bounds on the transitions that relate to the occurrence of a special clock transition tick. Concurrent real-time programs, nondeterministic timed Petri nets and diverse mechanisms for timing, synchronization and communication constructs can be converted into TTMs in a straightforward manner. € A declarative specification language called real-time temporal logic (RTTL) for describing the requirements that a TTM should satisfy without discussing how the TTM is constructed. RTTL is a timed extension of linear temporal logic augmented with a transition variable for describing TTM events. € Analysis techniques for demonstrating that a TTM conforms to its specification. Model- checking and a proof system for theorem proving are the main analysis techniques. Model-checking is a method for automatically verifying concurrent systems in which a finite-state model of the system (TTM) is compared with a correctness requirement (RTTL). Since time is a monotonically increasing variable, the state-space of naive timed systems is automatically infinite state. Hence, special care is taken in the model- checking algorithms to keep the state space finite provided the data types are finite. € A toolset called StateTime [38] which has a visual statechart-like executable language for representing TTMs hierarchically. An automatic translator to the model-checker and theorem prover STeP [31] allows for analysis. Although STeP is designed for untimed systems, the automatic translation is done in such a way so as to allow for the use of STeP¹s model-checking facilities. The STeP theorem prover can also be used for simpli- fying properties. The TTM/RTTL framework was initially conceived for the analysis of closed systems whose behaviour is completely determined by the state of the system itself [17]. In a closed system, we assume that the environment may set the initial values of input vari- ables, but, once the system starts running the environment cannot modify any of the sys- tem variables. Thus, all changes to the system variables are accounted for by the transitions of the program. By contrast, reactive systems are best thought of as open sys- tems whose behaviour depends on continuous interaction with the environment. We pro- vide below an informal sketch of how the framework is extended to the open setting. The concepts will be made precise in the sequel. This paper defines the notion of an open real-time reactive module where i is the module interface stub (e.g. variables or channels shared with the environment), b its body (a TTM) and s the module specification (an RTTL formula in the interface variables). The module specification s must hold for all module computations including arbitrary changes that the environment might make at any time to the interface variables. The com- position of two modules is also a module. Not all parts of a module are always determined. For example, the interface stub and specification may be given, but not the body. We denote a module with an unspecified body by . A Composition Rule (justified in the sequel) given by Composition Rule:        states that if each of the modules satisfy their respective specifications, then the system satisfies its global requirement provided the requirement can be derived from the con- junction of the module specifications. The composition rule allows for both bottom-up and top-down design. In the bottom-up method, the independently designed and implemented modules (with respective specifications ) when brought together exhibit the emergent property r provided . In top-down development, the system under design (sud) that is required to conform to a global system requirement r can be decomposed into modules and provided . At this stage, we have not yet committed to module implementations. Each of these modules can then be given to a programmer whose job it is to develop a body that satisfies the module specification. The body of module , whose variables can be reduced to finite ranges, can be shown to satisfy its module specification (i.e. ) by model-checking provided the effects of the environment are taken into account. The proof of , except in the simplest of cases, requires the use of deductive techniques (RTTL theorem proving). Thus the com- position rule usually involves a combination of algorithmic and deductive techniques. It is advisable that the programmer design and code the body of a module at as high a level as possible (using TTMs). This keeps the body simple and small which makes it understandable and prevents state explosion. There is then a need to refine the high-level module body into a TTM that is closer to implementation. For example, an abstract TTM may directly specify a delay of 50 ticks, but the implementation on a microprocessor might be a loop construct that increments a counter every traversal of the loop. The inter- nal loop and counter are unobservable to an external agent interacting with the module as the agent can only observe changes in the interface variables. Two modules with the same interface are observationally equivalent (written: ) if they agree on timed observations of their interface variables. Under suitable conditions (presented in the sequel) a Refinement Rule states that: Refinement Rule:          for any module specification s. Hence, if is observationally equivalent to , then can replace wherever it occurs with a guarantee that any module specification will be preserved. There are effi- cient polynomial algorithms for checking observational equivalence of finite state sys- tems, and equivalence preserving transformations are available for refining infinite state systems. Given a requirement r that a system sud must satisfy, the composition and refinement rules allow for a systematic modular development method represented by the tree in Fig. 1. Each step imposes a proof obligation as shown in the right hand column of the fig- ure. The process continues until all the modules have bodies that can be directly coded into the given program language. We need not adhere to the ordering suggested by the fig- ure. For example, the complete implementation of can take place before the other modules are designed. It is also possible to reverse-engineer already implemented code and move bottom-up. FIGURE 1. Structure diagram for compositional design method We proceed as follows in the rest of this paper. In section 2 we provide background information needed to understand the TTM/RTTL framework and the StateTime toolset. Section 3 defines the notion of a module, modular validity and the composition rule. It also describes how conditional specifications can be used to constrain module environ- ments. Section 4 presents the refinement rule for modules based on the notion of observa- tional equivalence of TTMs developed in [26]. Observational equivalence of TTMs will be defined precisely in the sequel, but the reader is referred to [27] for a set of TTM equiva- lence preserving transformations and to [28] for an efficient polynomial time algorithm to check TTM observational equivalence. Module observational equivalence is defined in such a way that the TTM results can be applied directly to module equivalence as well. In Section 5, we use the composition and refinement rules for the structured design of a reac- tor shutdown system. The design method is also discussed in some detail (Sect. 5.6). Com- parisons to other approaches and concluding remarks are presented in Section 6. 2.0 Background In the sequel, we use relative quantification where Q is a quantifier (" or $), T is the type of the dummy variable x, R is the range of the dummy variable and P a predicate [14]. For example, means ³for all values of an integer variable i, if i is at least as large as 3 then i has property P². If no range is supplied then it is true. The notation generally means that . For example, means that we are defining by . In TTM update functions (see sequel), denotes assignment, i.e. . 2.1 Real Time Temporal Logic (RTTL) Linear time temporal logic [32] uses temporal connectives such as h (henceforth),    (next), e (eventually), U (until) and past operators such as (previous state) to represent qualitative temporal properties. The standard connectives are applied to state-formulas (which are the atomic predicates) to obtain temporal logic formulas. Real-time temporal logic (RTTL) is obtained by adding a fair tick transition and the ability to refer to system transitions via a distinguished transition variable. We refer the reader to [32] for a precise discussion of standard temporal logic and to [37,40] for real- time temporal logic. We now provide a brief review of some of the basic concepts. Let and be the system variables where the type of is the integers and has a set type. An example of a state-formula f is . In this formula, the bound variable is just a dummy variable and is not considered a system variable. A state is a mapping from the system variables to values in their relevant types. Since evaluates to true in the state given by , we write (state s satisfies f), and we call s an f-state. A temporal logic formula such as (³eventually is true²) cannot be interpreted in a single state; rather it is evaluated in an infinite sequence of states given by where (³ satisfies ³) will mean that there is at least one state subsequent to the initial state that is an f-state. An inductive definition of the satisfac- tion relation can then be given. Let denote the satisfaction of temporal for- mula f at a position of the sequence . For a state-formula , . We can then give the appropriate inductive definitions for the propositional connectives (e.g. negation, conjunction, implication) followed by the usual definition of the temporal operators. For example, for temporal logic formulas g and h, the until operator is defined by . For an arbitrary tem- poral logic formula , is an abbreviation for . A formula is generally- valid iff . The implication () states only that ³f implies eventually g² at the initial posi- tion of the computation, i.e. if holds at the initial position then there is a subsequent posi- tion where holds. As a notational convenience, we will write for which states that the implication holds at all positions of the sequence. In general, the dou- ble arrow entails operator is defined by   for any temporal logic for- mulas p and q. We need the notion of timed transition sequences for the description of real-time sys- tems. Since we envisage that a transition causes a transfer from state to state , we may rewrite the infinite sequence of states as: (Eq. 1) The start transition (e.g. a computer reboot) puts the system in state . The transition takes the system from state to and so on. We give the initial transition the spe- cial name start. The distinguished variable (the transition variable) is always part of the state. The transition variable is used to record the last event taken, i.e. for the sequence we have that and . The reason we need a start transition is so that , like all other state variables, has an initial value. The transition variable can be used to refer directly to event occurrences. For example, for a traffic system, the temporal logic formula asserts that anytime the light turns red, it must eventually turn green. In order to represent time, we introduce the special transition tick. A timed sequence must satisfy the ticking constraint which asserts that there are an infinite number of ticks occurring in the sequence, i.e. . Thus, time must progress irrespective of what happens in a system or its environment. It is possible for any finite number of transi- tions to occur between two ticks of the clock. We may use quantified Manna-Pnueli temporal logic to define the bounded real-time until operator, , which in turn can be used to express a variety of important real- time properties. Informally, the meaning of the bounded until operator is that eventually will occur at a time between and ticks from now; until then must hold. Other bounded operators can then be defined as follows: Bounded response: p must hold after the l-th tick but before the -th tick. must hold before the -th tick. Bounded invariance: must hold until the -th tick. Exact time: is true in exactly ticks. The formula asserts that p will hold before the next tick of the clock. Several state changes can occur before p occurs without the clock advancing. The operator can often be used in place of the next operator where there is a need for stuttering-invariant for- mulas, i.e. formulas that are ³robust² with respect to unobservable moves of the environ- ment. Some further examples of clocked properties are: € : If holds initially, then eventually between 3 and 7 ticks holds, and must hold continuously until then. This property is asserted only at the initial posi- tion. € : Every position satisfying is followed within 4 ticks by , and holds continuously until then. € : If p holds at a position, then at some subsequent position before the next clock tick there should be the start of an interval of duration 2 ticks during which q holds continuously. € : The property cannot become true sooner than 3 ticks after any occurrence of the property . We often need to compare expressions in consecutive states. We therefore introduce an abbreviation for the next value of a variable , written . For example, the formula asserts that the value of is greater in every successor state that it is in its immediate predecessor (see [32] for the precise details). 2.2 Timed Transition Models (TTMs) TTMs are timed extensions of the fair transition systems of Manna and Pnueli [32]. The extension involves lower and upper time bound constraints on transitions, that refer to the number of occurrences of the special transition tick. A TTM M is defined as a 4-tuple as follows: € : a finite set of typed system variables. The distinguished transition variable is always in V, where . The variables set also include control and data vari- ables that are used to describe the various parts of M. Each state of M is a map from V to its types; the set of all states is denoted by (or just when it is clear what the TTM is). € I: the initial condition. This is a satisfiable boolean valued expression in the system variables that characterizes the states at which the execution of the TTM can begin. A state s satisfying I is called an initial state. € T: a finite set of transitions which includes the distinguished transitions start and tick. Each transition is a function that maps a prestate s in to a (possibly empty) set of -successor states . An empty successor set means that the transition is disabled (i.e. cannot be taken from the prestate). A successor state is also called a poststate of from s. If the set of successor states consists of a single post- state, then the transition is deterministic. If there is more than one poststate, then the transition is nondeterministic. € F: a fairness set where . Informally, the fairness constraint for each transition disallows computations in which is enabled infinitely often but is taken only finitely many times. Since, in general, we do not need nondeterministic transitions, we can also describe a transition by its enabling condition (the condition under which the transition becomes eligible to be taken), and a simultaneous update function where and are expressions in the system variables, which indicates that the values of in the poststate are respectively, where is the prestate. No other sys- tem variables (e.g. ) are changed. The transition is enabled in a state s (written: ) if ‹ otherwise is said to be disabled. The transition can be fully characterized by a transition relation given by which is a predicate in the primed and unprimed system variables. Primed variables refer to the value of the variables in the post- state, and unprimed variables refer to values in the prestate (see [32] for precise details). By convention, we leave out conjuncts such as for which there is no change. In addition to the enabling condition and update function, we associate with each non- tick transition a lower time bound and an upper time bound , where . We allow bounds and but not . The meaning of these bounds will be defined formally in the sequel, but we first provide an informal overview. A timed transition with lower time bound ticks and upper time bound ticks, must delay l ticks before being taken, but must be taken by u ticks of the clock, provided it remains continuously enabled, and is not disabled by the occurrence of another transition that might have the effect of disabling . The operational semantics of TTMs will be described by the set of all its behaviours called trajectories. Informally, a trajectory is a timed sequence of states that starts in an initial state satisfying the initial condition of the TTM. From any state of the computation, any enabled transition is taken in one atomic step. Either a tick transition is taken at each step, in which case time advances, or a non-tick transition is taken, in which case time stays the same. The resulting interleaving of enabled transitions allows us to model con- current processes. When the transitions are taken, they update the variables according to the transition update function. The clock must tick infinitely often in any computation, and an arbitrary but finite number of (non-tick) transitions can be taken between any two ticks of the clock. The lower and upper time bounds of transitions must be respected. A computation of a TTM , where for and , is a timed sequence satisfying the three constraints below. In each case, we show how to write the constraint as a temporal logic formula. 1. Initialization constraint: The first state of the computation satisfies the initial condition, i.e. . The initialization constraint is thus represented by the tempo- ral logic formula . The transition start occurs once at the beginning of the computation and never again. 2. Succession constraint: , i.e. every prestate at position i must have as its successor a poststate according to the update function of (the transition taken at position i). The succession constraint can be expressed in RTTL as , where is the transition relation for . 3. Fairness constraint: For each transition in the fairness set, it is not the case that is infinitely often enabled beyond some position in the trajectory, but taken at only finitely many positions in the trajectory.The fairness constraint can be written in temporal logic as . A timed sequence that satisfies the above three constraints is called a computation of . A computation describes the behaviour of a Manna-Pnueli fair transition system (enhanced with the tick of timed sequences). To describe the behaviour of timed transition models, we further constrain computations by lower and upper time bound constraints and call the resulting computations trajectories. 4. Lower bound constraint: for every transition with lower bound , if is taken at position j of the computation, then there must exist a prior position so that there are at least ticks of the clock between and , and , i.e. is enabled but not taken in the states . 5. Upper bound constraint: for every transition with upper bound , if is enabled at position j of the computation, then there must exist a subsequent position with no more than ticks of the clock between and , such that either is taken or dis- abled at position k. As with the initialization, succession, and fairness constraints, both the bound constraints can also be described in RTTL. For a non-tick transition with lower time bound (where ) and upper time bound , the bound constraint is: (Eq. 2) where , and where (the previous tem- poral operator) holds at a position of a trajectory provided is not the first position of the trajectory and holds at position . If , then the left conjunct is replaced by true. If , then the right conjunct of the consequent in (Eq. 2) is replaced by true. The bound constraint (for both lower and upper bounds) can be written in tempo- ral logic as: (Eq. 3). The moment of enablement describes the relevant positions of a computation at which the bound constraint for a transition (that is enabled at that position) must be asserted. A relevant position is either the initial position , or a position at which the transition has just been taken and is re-enabled, or a position where has just become enabled . Once a transition becomes enabled at some position, it begins to ³mature² but cannot be taken until its lower time bound number of ticks has been taken, at which point the tran- sition becomes ³ripe² for execution. If the transition is continuously enabled during matu- ration, then it can be taken any time after it becomes ripe, but it must be taken or become disabled before the upper time bound number of ticks has expired. Thus, transitions ³mature² together as time advances but execute separately in an interleaving manner. As noted above, the initialization, succession, fairness and bound constraints can be expressed in RTTL. The formula defined by (Eq. 4) fully describes the set of all trajectories of the TTM M. Since a trajectory of a TTM is a timed sequence, the trajectory must also satisfy the ticking constraint . However, there is the possibility of a conflict between the upper bound and the ticking constraint (in which case no timed sequence will satisfy and the ticking constraint simultaneously). This happens in the presence of immediate transitions of the type that are self-loops ‹ such a is taken repeatedly yet the tick transition is delayed indefinitely. This is called a Zeno computation and the TTM is said to exhibit Zeno behaviour. Any cycle of transitions whose elements are all immediate may also exhibit Zeno behaviour. A TTM that exhibits Zeno behaviour cannot be implemented, and hence we must find ways to ensure that our systems are non-Zeno. The problem of Zeno computations can be avoided by disallowing self-looping imme- diate transitions. However, immediate transitions are useful for modelling ³instantaneous² (i.e. before the clock ticks) reactions. If immediate transitions are used in a TTM M, then we must check for the validity of in every single computation that satisfies the bound constraints. Fortunately, for those systems where model-checking can be used, the ticking property can be verified automatically (e.g. see Table 1 in Sect. 5.5). In the sequel, we assume that all TTMs are non-Zeno. This is not restrictive at all for the exam- ples of this paper because all TTMs can be model-checked to ensure that they are non- Zeno. The set of all trajectories of a TTM is denoted by . If a trajectory satisfies a temporal logic formula , then we write . If an RTTL formula is satisfied in all trajectories of (i.e. ), then we write , and the formula is said to be M-valid. Any generally-valid formula is also M-valid. Any trajectory in always satisfies ; hence, the transition system M and the temporal logic formula are two equivalent ways of describing . Theorem 1: For any (non-Zeno) TTM M and RTTL formula p in the variables of : (a) , and (b) . If we treat as an axiom of the RTTL logic, then (Th. 1)(a) describes the relative completeness of the logic for proving M-validities. An oracle is a device that is guaranteed to provide a proof of any generally-valid RTTL formula. Hence to prove the M-validity of p it is sufficient to submit to the oracle the formula . While the axiom is theoretically adequate it is not very practical. In practice the special proof rules in [36] and model-checking (Sect. 2.4) are the preferred methods for proving M-validities. 2.3 Parallel composition of TTMs The parallel composition of two TTMs and is defined in [40] by: € , € provided is satisfiable, € where and hence , and € where . We call the composite TTM. The above definition holds for shared variables but must be slightly modified for synchro- nized transitions or channels as described in [40]. Both and synchronize with respect to the start and tick transitions. The tick transition thus provides the composed sys- tem with a uniform notion of time. 2.4 Overview of the StateTime toolset The StateTime toolset assists the user (a) to describe devices and systems using a graphical structured language, (b) to execute the description so as to validate that the description is a reasonable model of the actual system, and (c) to check that the description conforms to its requirements using model-checking. We give a brief description below of the main features of the toolset needed for the sequel. The reader is referred to [38] for a more complete description. The main parts of the toolset of interest to us are the Build tool and its translator to the theorem prover and model-checker STeP [31]. The Build tool is a window-based front end for constructing compact visual models of real-time systems called TTMcharts. TTM- charts resemble statecharts, but with a simpler semantics and with the additional feature that transitions may have time bounds. We often use the terms TTMcharts, charts and TTMs interchangeably as the semantics of TTMcharts is based on TTMs. A chart is a hierarchy of objects. Objects describe control information and impose structure on the operation of the system. An object is either primitive, parallel (called AND in statecharts) or serial (XOR in statecharts). A primitive object has no internal structure. A parallel object is constructed from a collection of child objects (or sub- objects) by parallel composition. The parallel composition of child objects operates in all of these child objects simultaneously. The entry into a parallel object via an event causes the simultaneous entry into each of the child objects. The exit from the object causes the simultaneous exit from all its children. A serial object is constructed from a collection of child objects such that only one of the children operates at a time. The entry and exit from a serial object via an event causes the simultaneous entry and exit of the currently operat- ing child object. Charts may have data variables which are tested and set by events. Each non-primitive serial (XOR) object has an object variable which is used to indicate which of its children is currently operating. As an example, consider the plant chart (Fig. 2) which will be described in more detail in Sect. 5.2. The plant is the parallel composition of two children called relay and output which we write as . The serial object relay has two children closed and open which are primitive. Zooming in to the output object indicates that it is the serial composition of the primitive object wait and the sub-object update. The update object is the parallel composition of the pressure and power sub-objects which is where the pressure and power sensor values are updated. FIGURE 2. Plant module module plant(C;P,W) in C: {0,1} where /* relay activation. causes the relay to open */ out R: {closed, open} where /* Relay position variable */ out P: {0,1} where /* pressure variable where is high pressure*/ out W: {0,1} where /* power variable where is high power*/ Body private D: {wait,update} Specification (Eq. 5): The above module specification, inherited from Fig. 3 for the relay, is modularly-valid. end module plant The top-level objects relay and output have object variables and respectively where and . The state-formula defined by describes a state in which the relay is closed and the next sensor update is two ticks away. The pressure and power are examples of data variables. A serial object begins execution at its default indicated in bold; e.g. the default for the output object is wait (Fig. 2). Once a cycle[0,0] event is taken in the output object, nothing else can happen until two ticks of the clock are taken. After two but before the third clock tick, the endupdate[2,2] event must occur (in this case, there are no other events to preempt its occurrence). Before endupdate occurs, the pressure and power, or just one of them, or no update at all may occur. The source of the endupdate event is the structured object update; hence endupdate can be taken, no matter where execution in update currently resides, and preempts the internal events of update. A user can describe systems incrementally by composing sub-objects together to form a super-object (bottom-up), or by decomposing a object into further sub-objects (top- down). A chart can be executed at any point in the development cycle even before it is finally fixed using the interactive simulation tool. The simulation tool displays chart trajec- tories, and requires user interaction to select the transition to be taken at nondeterministic selection points. The Build tool automatically translates TTMcharts into fair transition systems according to the algorithm presented in [39]; STeP [31] can then be used to model-check the chart for conformance to its specification. The current StateTime toolset was not meant for modular systems. It suffers from vari- ous deficiencies including the fact that it does not support interface stubs, automatic gener- ation of module environments (Sect. 3.0) and refinement. It is easy to verify standard temporal properties, but an observer must be constructed for real-time properties. How- ever, the tool is used in this paper for the construction of modules, their environments (done manually) and model-checking module properties. In principal, a chart when loaded into STeP can also be verified using theorem proving ‹ however, theorem proving real- time properties proved tedious (especially on account of the need to use quantifiers). We are currently updating StateTime to fully support real-time modules and real-time formu- las for both model-checking and theorem proving in a seamless fashion, based on the results of this paper. 3.0 Modules and module composition Our notion of a module is based on the untimed reactive modules of Manna and Pnueli [32]. Although the Manna Pnueli framework has been used for real-time systems [23], the extension to their system for modules as delineated by Chang [8] is different to ours. The main differences are: (a) our modules are supported by a model-checker, (b) we provide a state-event refinement relation for modules, and (c) the reactive modules of [32] are not fully compositional as their parallel composition yields a transition system, not another module (composition of our modules yields another module). We now explain these differ- ences in more detail. Chang [8] advocates a restricted assumption/guarantee style, wherein the environmen- tal assumption is stated as a restriction on the environment¹s next-state relation. He also presents a decision procedure in the propositional case and a deductive system for the dis- crete time metric temporal logic used for transition modules. Although Chang provides a deductive framework for real-time modules, he does not present model-checking algo- rithms and tools (which are crucial for the needs of this paper). Chang¹s temporal operators are new; they are not expressed in ordinary untimed tempo- ral logic. The transition modules of [8] must be self-disabling, i.e. once a transition is taken it cannot be again enabled (as in a self-loop). The TTM semantics of modules in this paper does not impose this restriction on module descriptions. The untimed refinement relation of [32] will not work for real-time modules (as will be explained in Sect. 4.0). Hence, in Sect. 4.0, we introduce the necessary framework needed for real-time module refinement. The reactive modules of [32] are not fully compositional as their parallel composition yields a transition system, not another module. In this section, we provide the notion of a fully compositional discrete time transition module (like [8]). This requires a more com- plete treatment of the notion of the interface stub and modes of variables in a module. It also allows our treatment to deduce the trajectories of the composite module given its sub- modules (Lemma 1), from which we obtain the notion that a module specification must be satisfied independently of the behaviour of the environment (Lemma 2), and finally yields the Composition Rule (Th. 2). By contrast, [32] starts with the notion of a module as given in Lemma 2 and then proceeds from there to obtain the Composition Rule. A module is defined by its interface stub , body and RTTL specification : 1. The interface stub consists of the declaration of all the variables that are shared between module m and other modules in its environment (defined more precisely in Sect. 3.2). The stub also declares the initial values of all the shared variables. We let denote the set of shared variables. 2. The body is a program whose statements may refer only to variables declared private to the body, or to variables in the interface. The set of private variables is denoted . In the sequel, the body is a TTM, in which case we let denote the TTM with variables set . The initial condition is the conjunction of all the initial conditions declared on both the private and interface variables. 3. The specification of the module is an RTTL formula in the shared interface vari- ables. The specification asserts the required visible behaviour of the module. In order to describe the behaviour of a module in an environment that may arbitrarily modify the interface variables , we adjoin to the module TTM a spontane- ous environmental transition defined by the update function (i.e. the interface variables can take on arbitrary values) while all the private variables remain unchanged, i.e. . Thus the environmental transition may exhibit arbitrary behaviour, except that it may not modify any private variables of the module. However, shared interface variables may be changed at any point to any value in their respective types. Definition 1: [The TTM associated with a module] The TTM associated with the module is defined as where and where is the set of transitions of the body TTM, and is the set of fair transitions of the body (note that ). Since is a TTM, we define and where is the set of all pri- vate variables, i.e variables in . (As before, we require that the timed transition model be non-Zeno). The succession constraint of allows the body transitions to be interleaved in an arbitrary fashion with the environmental transition. The environmental transition thus simulates the behaviour of the module in an arbitrary context and allows the module to take stuttering steps in which none of the module private variables change from the prestate to the post- state. The existentially quantified formula in (Dfn. 1) describes the same system as except with the private variables hidden, and thus this existential formula can be considered a description of by abstract implementation [32, p.340]. In this style of description, we may choose the most straightforward implementation of the module and describe its operational behaviour using a TTM (e.g. if is a buffer, then a private list variable may be used to remember sequences of messages). What makes the implementa- tion abstract is the existential quantification of the private variables. This means that we do not require or imply in any way that the real implementation of the module should contain any of these private variables (e.g. the list variable in the case of a buffer need not be used). Definition 2: [Modular-validity] The RTTL formula p is modularly-valid for the mod- ule m (written ) iff . 3.1 Parallel composition of modules Modules (with variable sets ) for are said to be compatible with each other if: € each module has private variables that are not variables of the other module, i.e. and , and € the conjunction of their initial conditions is satisfiable, i.e. is satisfi- able, and € the conjunction is satisfiable. Compatible module composition, , is defined by where , i.e. some of the interface variables of the sub-modules may be hidden at the parent level. is ordinary TTM composition (Sect. 2.2). Finally . The private variables of the composite is , and the initial con- dition is defined by . The super-module is itself a module; the TTM associated with this super-module is just the TTM obtained from together with the environmental transition that may change only variables in (i.e. it may not change any private variables). In the next lemma, we assume that we have two modules and . If an environmen- tal transition in a trajectory of module has the same effect on its interface variables as a transition of , then we relabel the environmental transition in the trajectory to , and the set of all the relabelled trajectories of we call . A symmetric definition also provides us with the set of relabelled trajectories of . Lemma 1: If then . Proof: Let . Trivially and hence the initialization constraint of is satisfied. For the succession constraint, consider any position of . Either the environment transition is taken at position or some transition of is taken. The environ- ment transition of may not modify any private variables of m and hence may also not modify private variables of , so any environment step of is also an environment step of . If some transition of is taken at position , then it is either a transition of or of that is taken. Since no transition of may modify private variables of , a step taken by a transition of (say ) is the same as an environment step relative to (the transition must be renamed to an environmental transition). Thus at any position either a transition of is taken or an environment transition of is taken, and hence the suc- cession constraint holds. The fairness constraint of is also satis- fied, as any transition of that is enabled infinitely often but not taken would also violate the fairness constraint of . The ticking constraint of is also satisfied, for suppose there is a position of beyond which there is no tick of the clock for , then the ticking constraint for would also be violated. If a transition of violates its bound constraint, then the bound constraint on transitions of will also be violated. Hence must also sat- isfy the bound constraint of . Since satisfies the initialization, succession, fairness, ticking and bound constraints of , it follows that holds. By symmetry it also follows that holds. Thus . For the converse, let . At any position of either a transition of or of is taken, in which case the same transition belonging is taken, or an envi- ronment transition that is an environment transition of both and is taken. This envi- ronment step must also be an environment step of as no private variables of and could have been changed. We can make similar arguments as before for the other con- straints but in the converse direction. Hence . n Lemma 2: Let modules and be compatible. Then (a) , and (b) For a module m, for any compatible module and RTTL property . Proof: Follows directly from Lemma 1. n Recall that a property is modularly-valid only if it is satisfied by all trajectories of the module. Lemma 1 tells us that the trajectories of the super-module are always a subset of those of its sub-modules. This means that a valid specification of a sub-module must also be valid for the super-module (Lemma 2a), and that a module specification remains valid no matter what the behaviour of its environment is, provided the environment respects the compatibility constraints (Lemma 2b). Theorem 2: [Composition Rule]. Let and be any two compatible modules and let the general-validity given by hold. Then . Proof: Follows directly from Lemma 2 and temporal logic. n As mentioned in the introduction, the Composition Rule can be used bottom-up or top- down. In the bottom-up method, pre-existing implemented ³off the shelf² modules can be combined into a super-module that satisfies a system requirement r. In the top-down method, we proceed as follows: 1. The system architect decomposes the system under design () into modules and by: (a) designing compatible interface stubs and , and (b) designing module specifications such that . 2. The architect gives each module interface and specification to a programmer. It is the job of the programmer to develop the module body so that the specification is modu- larly-valid. For example, if the programmer is given and for the first module, he must design a body so that where the module is fully described by . 3. The required system is then which is guaranteed by the Composition Rule to conform to the requirement . Parts of the development method can be automated by using a combination of model- checking for proving modular-validity (step 2), and deductive theorem proving techniques can be used for proving that the system requirement is a consequence of the module spec- ifications (step 1b). A compositional proof has the following outline: 1. is modularly-valid for (by model-checking) 2. is modularly-valid for (by model-checking) 3. general-validity (deductive theorem proving) 4. 1, 2, 3 and the Composition Rule where In the sequel, we will leave out the module satisfaction symbol (except for its appearance in the last line) and write the above proof as: 1. is modularly-valid for 2. is modularly-valid for 3. general-validity 4. 1, 2, 3 and the Composition Rule where By Lemma 2 (b), once we know that the context of the proof is the module , then any specification of a sub-module of will also hold for , and hence there is no need to indicate which sub-module specification we are dealing with. 3.2 Modes of interface variables The interface stub of a module defined in the previous subsection consists of a set of typed shared variables with their initial conditions. We can provide more structure and flexibility to the interface specification which will enhance the user¹s ability to understand a module. The additional structuring mechanism is provided by describing the modes of the shared variables. A variable in the interface stub is either in (the module body can read the variable but not write to it), out (the environment can read the variable but not write to it), or share (both the body and the environment have write access): interface_stub ::= {mode {variables}+ : type [where init]}* mode ::= {in | out | share} If a module m has a declaration ³out ², then no other module in the environment of m may have a writing reference to the variable . If two (or more) modules each write to y, then they must each have the declaration ³share ², thus indicating that the external envi- ronment may also change . Let the variables in the interface stub be , where are the ³in² and ³share² variables (i.e. all variables whose value may be changed by the envi- ronment), and where are the remaining interface variables (the ³out² variables that the environment does not change). We often refer to the module by , where the semicolon separates the out variables from those that the environment can read and modify (the in and share variables). Definition 5: Two modules and are interface compatible, provided each vari- able satisfies the following constraints: the types declared for in both interfaces match, the conjunction of their where clauses (supposed true when not specified) is satisfiable, and if one of the declarations specifies an out mode, then the other specifies an in mode. The reactor trip relay module relay (taken from the example in Sect. 5.2) is shown in Fig. 3. When the command to open the relay () comes from the environment, then the relay is immediately opened () before the next clock tick, thus shutting down the reactor. The specification of the relay (see (Eq. 6) in Fig. 3) does not contain the next operator in the consequent; instead, the operator is used. This is because the trajectories of a module may have environmental steps that leave the state unchanged. Specifications must therefore allow such ³stuttering² steps otherwise the specification will not be modularly-valid. FIGURE 3. The relay module module relay(C;R) in C: {0,1} where initially /* when the input command is given, the relay is opened, and when the relay is closed */ out R: {open, closed} where initially /* R is the relay object variable that is exported as readonly output */ Body TTMchart (using the StateTime Build tool) Specification: (Eq. 6): /* Informal description: The operator is needed in the consequent. Although the relay responds to a stimulus (i.e. a change in C) before the next clock tick, the reponse is not immediate but may occur a few states later (as actions of the environment are interleaved with actions of the relay). The above specification is modularly-valid */ end module relay. 3.3 A small example of compositional reasoning The module (Fig. 4) is part of the DRT controller which will be discussed in the sequel. The controller consists of three independent microprocessors, each one with independent sensors of reactor power and pressure. Each microprocessor controller signals through a variable whether to open the relay (which shuts down the reactor), or to close the relay (allowing the reactor to be started up again). The in variables of majorVote are thus , and the out variable is , which is set to 1 when the majority of the microprocessor vote for opening the relay (i.e. when ). The specification can be shown to be modularly-valid by model-checking. FIGURE 4. Module for majority voting logic module majorVote(C1,C2,C3;C) with bitType={0,1} in : bitType;   /* 1 stands for a vote to open the relay, and 0 to close the relay. */ out : bitType where initially  /* Only majorVote can write to to set the relay*/ Body private : bitType where initially /* majority vote object variable*/. Specification (EQ 7): /*Informal description The first line of the specification states that once the majority of microprocessor controllers vote to open the relay, and this vote remains in place for time 20 ticks, then within one tick of the clock, the output variable will be set so as to command the relay to open, and will remain set for 20 ticks of the clock. The second line states a similar specification for the command to close the relay. */ end module majorVote The relay module (Fig. 3) and the voting module (Fig. 4) are interface compatible. We may therefore use the modularly-valid module specifications (Eq. 6) and (Eq. 7), and the Composition Rule to prove the validity of (Eq. 8) where p is defined by: (Eq. 9)p: The proof of the first conjunct of (Eq. 9) is as follows: 1. by modular-validity of (Eq. 7) 2. by modular-validity of (Eq. 6) 3. (2) and RTTL 4. (3) and RTTL 5. (1), (4) and Composition Rule The temporal logic reasoning is performed in the RTTL proof system. For example, the RTTL theorem used in step (3) is: . The Composition Rule provides a powerful technique for beating combinatorial explo- sion of states. To verify a global requirement r of a system composed of modules, it is not necessary to deal with the complete system (e.g. by generating its global reachability graph). Instead, we need only verify the specification of each of its objects one at a time, provided we can show that the object specifications entail the global requirement. The modular-validity of module specifications for a module can be determined by applying the model-checking and theorem proving tools of StateTime (Sect. 2.4) to the TTM that corresponds to . For example, the relay module specification in Fig. 3 can be proved modularly-valid by model-checking the set of transitions associated with the body together with the nondeterministic environmental transition with update function choose(C), which allows the input variable C to vary arbitrarily. In the above relay example, an unrestricted environment was used to check the modu- lar-validity of the module specification. This is not always possible as an unrestricted envi- ronment can sometimes generate larger intermediate reachability graphs than the reachability graph obtained when the environment is limited to a known set of fixed mod- ules. This is because certain states of the module in an unrestricted environment may be unreachable in the composite. There are two ways to address this issue: either (a) decom- pose the module into smaller sub-modules where an unrestricted environment will not be problematic, or (b) restrict the environment of the module to the actual environment in which the module is expected to operate. The easiest way to restrict the environment involves the use of conditional specifica- tions for the module of the form which asserts that if the environment is assumed to behave according to the RTTL formula then the module is guaranteed to behave according to the RTTL formula . In other frameworks, such conditional specifications are called assumption/guarantee properties [22], and special rules are provided for reasoning about them. In our framework, conditional specifications are no different from any other module specifications. Our purpose will be to show that is modularly-valid for the module , i.e. . This does not contradict our definition that a module specification should hold independently of what the environment does. The property will indeed hold true only if the module environment behaves according to . However, holds for the module in any environment; this is because if the environment does not satisfy , then need not hold true [32, p.356]. In the sequel, we deal with modules that are intended to work in fixed environments. For example, the environment of the DRT controller module (Sect. 5.0) is the plant which will remain fixed throughout the design. Consider a conditional specification for one of the controller sub-modules which asserts that if the plant (which is the environment of m) behaves according to then m will behave according to . To verify the modular-validity in an unrestricted envi- ronment in which the plant output variables can take on any value at any moment, will generate a larger reachability graph than necessary because there will be states that are not reachable in practice. The actual plant sensors are filtered and hence change only every two ticks of the clock. Thus we do not need to consider all the possibilities generated by continuously changing sensor values. Instead, we can verify which will involve a smaller reachability graph in which plant changes occur only every two ticks. The following theorem justifies this procedure. Theorem 3: Let and be two compatible modules and p an RTTL formula in the interface variables. Then . Proof: < (Th. 1)(a)  > < propositional temporal logic > < Composition Rule and holds for by (Th. 1)(b) > . n 4.0 Module refinement If a module m has been implemented with a given body, under what conditions can we replace the body with a new one while still retaining the same observed timed behaviour at the interface stub? One possibility is to use the notion of program equivalence of untimed concurrent programs developed in [32, p46]. However, this notion of equivalence will not work for our real-time reactive modules. Consider a program with two variables and . In [32, p46], a sub-sequence is reduced to if we want to observe variable . We have thus lost a record of one of the clock ticks, because in the refinement relation of [32], program states that are identical to their predecessors are omitted from the sequence. But, in real time sys- tems, it is essential that the reduced system show the same timed behaviour as the original system. We will thus need to define a notion of observational equivalence that takes into account state (data such as the value of ) as well as events (ticks of the clock). In this sec- tion, we adapt the state-event notion of observational equivalence developed in [26,27,28] to the needs of real-time reactive modules. Because we need to deal with both states and events, we also cannot just use the standard event-based notion of bisimulation [33], as will be explained in this section. Consider two modules that have the same interface stub but different bodies. For such modules we will define a notion of module observational equivalence that is composition- ally consistent and preserves any stuttering invariant RTTL module specification (detailed explanation follows below). Thus the first body can be replaced by the second with a guar- antee that any module specification that holds for the first will also hold for the second, and vice versa. Observational equivalence will allow us to refine an abstract module into one closer to code implementation. The abstract module may have a substantially smaller state space than the refinement and hence will be more amenable to model-checking. Informally, if a module is equivalent to a module having the same interface stub (written ) then preserves the timed behavior of over the interface variables. We want a notion of observational equivalence that only distinguishes between the two modules if the distinction can be detected by an external agent interacting with each of them. The agent can observe any of the interface variables and the start transition and tick of the conceptual global clock, but not any of the private variables or internal transitions which are unobservable to the external agent. We call such internal unobservable actions -transitions. Although an external agent may not be able to observe an internal transition itself, it may be able to observe the effects of the internal transition (e.g. if the internal transition changes one of the interface variables). 4.1 Observation equivalence of TTMs In [37], an algorithm is given for constructing the reachability graph of a TTM. The reachability graph is used as the basis for model-checking RTTL formulas, as maximal fair paths in the reachability graph correspond to TTM trajectories. We illustrate the concept of a reachability graph by referring the reader to the sample TTM with variables set as shown in Fig. 5. The reachability graph of is also shown in Fig. 5. The reachability graph is a labelled transi- tion system with state set , transition label set , is a set of binary relations on , and the initial state is . If and then holds precisely when (i.e. is a -suc- cessor of ) where are the restrictions of respectively, and both occur in tra- jectories of the TTM . Let be an abbreviation for which is called a - step from to . The notation denotes a sequence of steps in the graph. Any maximal sequence of steps in the reachability graph corresponds to a trajectory of the TTM respecting the initialization, succession, fairness, and bound con- straints (Sect. 2.2). The timed behaviour of the TTM in Fig. 5 is equivalent to with respect to the observable variable (in a sense to be made precise in the sequel). In this weakly observ- able setting, the and transitions are observable but no other transitions are visi- ble to an external agent. The observable variables set is ; we require that the variable be in the variables set of both TTMs. The TTM is much simpler than and has a smaller reachability graph (Fig. 5). We therefore call an abstract specifica- tion of the concrete refinement . FIGURE 5. Observably equivalent TTMs TTMs and are observationally equivalent, i.e. . For the precise definition of observation equivalence, we need the concepts of state pro- jection operators and unobservable -transitions. For a set of observable variables of a given TTM, the observable state projection operator tells us when states and agree when restricted to their observable variables. For example, if we are given the states , and the observable variables set , then as they agree on the component of the state. An external agent interacting with the TTM can observe the start and tick transi- tions; but the other transitions and are unobservable. Similarly, the transition in is unobservable. We will relabel the edges of reachability graphs so that all unobservable transitions are called . Although the -transition itself is unobservable to an external agent, its effect may be observable (e.g. when the transition is taken it may change an observable variable); however, the external agent is unable to tell which transition caused that effect. Definition 6: [State-event labelled transitions systems SELTS] Let be a TTM, and let be a given set of observable variables. Let the reachability graph of be where is a countable set of states and is the initial state. Then is a labelled transition system, called a state- event labelled transition system (or SELTS), where and where: (Eq. 10) (Eq. 10) achieves the required relabelling, i.e. all transitions in the reachability graph other than start and tick are now relabelled to the unobservable -transition in the corresponding SELTS. The following definition is needed for the weak state-event bisimulation: Definition 7: The unobservable move is defined by: The action of taking an observable step (i.e. is either start or tick) in a SELTS that has (possibly empty) sequences of unobservable steps on both sides is defined by: We also define a similar move for the unobservable -transition (which may or may not cause a change in the observable variables) by: We are now ready to define the notion of a weak state-event bisimulation relation. In the weakly observable setting with unobservable -steps, the steps and are indistinguishable, producing the same observations (or possibly lack of observation in the case of a move). Definition 8: [Weak state-event bisimulation] Let be state event labelled transition systems for the TTMs for with a common observ- able variables set . Then the relation is a weak state-event bisimulation relation if : and € implies € implies The above definition of bisimulation can be paraphrased by saying that two states are weakly bisimilar if any move from one of the states to a new state can be matched by the other state making a move, or sequence of moves, producing the same observations on both the observable variables and the observable transitions (start and tick) and reaching a state that is weakly bisimilar to the state reached from the first state. The standard notion of bisimulation [33] is defined with respect to the events of a labelled transition system. While it is possible to describe systems using only state infor- mation or event information, there are many applications where the use of both state and event information is quite natural. The above notion of (weak) bisimulation is defined not only with respect to the observable events of the labelled transition system (needed to maintain a global notion of time via the clock tick), but also with respect to the states of the labelled transition system (needed for dealing with properties involving the observable variables). For TTMs that must synchronize with each other via shared events (in addition to start and tick), the set in (Dfn. 6) can be expanded quite naturally to include any such additional synchronized events without the need to change the definition of bisimulation. Since weak bisimulations are closed under union, there is always a largest weak bisim- ulation relation (which we denote by the infix operator ) relating the states of to that of for an observable set of variables . Thus if (respectively ) is a state of the reachability graph of (respectively ) then we can write whenever . This leads to the notion of state-event equivalence of TTMs: Definition 9: [] Let (with initial state ) and (with initial state ) be two TTMs with variables sets and respectively. Let be a given observable set of variables. Then and are called state-event equivalent over (written: ) provided . Where the observable set of variables is fixed from the context to , we write . For the example TTMs in Fig. 5 with observable variables set , we have that . For finite state TTMs, [28] provides an efficient polynomial time algorithm for check- ing the equivalence of two TTMs. For possibly infinite state TTMs, [27] presents equiva- lence preserving transformations. The following theorems indicate the usefulness of state- event equivalence [26]. Lemma 3: (corollary of Lemma 2 in [26]) Given TTMs all having the same observable variables set, then Thus, state-event equivalence of TTMs is compositionally consistent, i.e. the designer can replace a TTM with an equivalent refinement with a guarantee that the observed time behavior will be unchanged. The set of SESI (state-event stuttering invariant) temporal logic formulas is defined in [26]. We will only need a subset of SESI formulas for the sequel, which we now define. An atomic SESI formula atomic_sesi of a module m is any state-formula, having no occur- rences of the transition variable , and whose free variables are the observable variables, i.e. the variables in . A SESI formula is defined by: (Eq. 11)sesi ::= atomic_sesi | | | | | The formula is SESI as it is derived from the bounded until operator which itself is SESI. Also is SESI because all the other temporal logic operators, except for next, can be obtained from the until operator. The operator can usually replace the next operator. It is shown in [26] that some formulas involving the next operator are also SESI, but we will not need these for the sequel. Lemma 4: (corollary of Theorem 3 in [26]) Let be a SESI formula with a given observable variables set . If and are TTMs such that then: . The above lemma is significant for model-checking. We may check an abstraction for conformance to rather than its more complex refinement , with a guarantee that will also hold for the refinement, provided the TTMs are non-Zeno. 4.2 Observation equivalence of modules The behaviour of a module was defined in Sect. 3.0 with the help of an associated TTM , which is the composition of the body TTM and an environment transition that arbitrarily changes interface variables . Definition 10: [state-event equivalence of modules] Let and be two modules having precisely the same interface variables (i.e. ). The observable variables set of these modules is defined as . The corresponding reachability graph of each of these modules is for from which their corresponding SELTS can be obtained as in (Dfn. 6). The state event equiv- alence of these modules is then defined by: . As with TTMs, one may check the conformance of an abstract module for conformance to its specification with the guarantee that the refinement will also satisfy its specification, as stated in the following theorem. Theorem 4: [Refinement Rule] Let be an arbitrary SESI formula for non-Zeno mod- ules and having the same interface variables such that . Then: . Proof: Since we have that where is the TTM corresponding to the module (Dfn. 1) for and . By Lemma 4, it follows that . Since the modules are non- Zeno, holds. Hence, by the definition of modular-validity (Dfn. 2) holds as required. n 5.0 Modular Design of the delay reactor trip (DRT) Industrial reactive systems are often specified using a combination of timing diagrams, pseudocode and careful English narrative. This has the considerable advantage that it is accessible and intelligible to a wide community. It has the disadvantage that even the most lucid informal descriptions are prone to omissions and ambiguities. More importantly, conformance analysis can only be undertaken in a more precise setting. In this section we describe an example taken from the actual requirements document for the shutdown system of an industrial nuclear reactor. We translate the informal descrip- tions and requirements into precise counterparts in the TTM/RTTL framework, and then use the modular development method developed in this paper to design the system and check its conformance to requirements. The abstract design so obtained can then be refined down to a format close to pseudocode suggested in the original requirements docu- ment. This is not the way the original problem was presented. Originally, the pseudocode was a given, and the engineers wanted to know if the pseudocode satisfied the informal requirements as presented in the timing diagram. This reverse engineering problem can be solved using the same compositional and abstraction techniques but working bottom-up (see [38] for the reverse engineering problem). 5.1 Informal description of the problem In early nuclear reactors, the shutdown systems were constructed of analog devices. The analog control had the virtue of being simple to understand but inflexible, unable to perform system checks and not always reliable. It was felt that the situation could be improved by installing computerized control with at least two independent shutdown sys- tems, designed by different teams, each shutdown system itself having 3-version control and majority voting logic [43]. The delayed reactor trip (DRT) problem was first described by Lawford et. al. [27]. Lawford developed behaviour preserving transformations for timed transition models (TTMs) with which he was able to discover a flaw in the proposed design [25] involving a single controller. However, the transformational theory cannot be fully automated as no set of transformations is complete for proving observation equivalence between the actual implementation and its abstract specification. In [38], the StateTime toolset was used to verify the single controller case, where it also helped to find a bug in the original specifica- tion. A corrected version of the pseudocode was shown to conform to its requirements by model-checking. In this paper we consider the case of 3-version control using a majority voting circuit to determine control actions. The StateTime toolset was not able to model-check the com- plete system due to a combinatorial explosion of states. However, using a combination of model-checking and deductive techniques in the modular framework, the conformance of the systems to its requirements can be demonstrated. The DRT for nuclear reactors used to be implemented in hardware using timers, com- parators and logic gates similar to the timing diagram shown in Fig. 6. The new DRT sys- tem is implemented on microprocessors. Digital control systems provide cost savings and flexibility over the hardware implementation. However, the question now is whether the new microprocessor based software controller satisfies the same specifications as the old hardware implementation. FIGURE 6. Analog implementation of the delay relay trip timing. The hardware version of the controller implements the following informal require- ments: [R1] When the power and pressure of the reactor exceed acceptable safety limits, the comparators which feed in to the first AND gate cause Timer1 to start. After 3 seconds, Timer1 sends a message to one of the inputs of the second AND gate indicating that the time- out has occurred. If after this first time-out the power is still greater than its safety limit, then the relay is tripped (opened), and Timer2 starts. The relay must remain open until Timer2 times out which happens after 2 seconds. Requirement [R1] ensures that the relay is opened and remains open for two seconds thus shutting down the nuclear reactor in a timely fashion. If the controller fails to shut down the reactor properly, then catastrophic results might follow including danger to life. By the same token, each time the reactor is unnecessarily shut down, the utility operating the reactor loses money because it must bring additional fossil fuel generating stations on line to meet demand. The next informal requirement states: [R2] If the power reduces to an acceptable level then the relay should be closed as soon as possible (thus allowing the reactor to operate once more). In the actual DRT, there are three identical microprocessors that have independent sensors for power and pressure. The final decision on when to shut down the reactor is based on a majority vote of the three microprocessors. The code is to be implemented on a microprocessor with a cycle time of 100ms. The microprocessor samples the inputs (pressure and power ) and passes through a block of code every 0.1 seconds. It is assumed that the input signals have been properly filtered and that the sampling rate is sufficient to ensure adequate control. In the formal model, one tick of the clock will represent 100ms. 5.2 Formal requirements The first step is to decompose the drt into two parallel modules the plant and the control- ler, i.e. . The plant corresponds to the part of the system that is fixed and known. The controller is the part of the system that must be designed. The observable variables of the DRT are shown in the data flow diagram of Fig. 7. The plant outputs are the relay position (), power () and pressure () variables. The input to the plant () is a relay activation variable that can be used to force the relay to open or close. In the absence of control, the plant can behave unsafely. For example, if pressure and power both go to unsafe levels, there is nothing to force the relay to trip. FIGURE 7. The observable inputs and outputs of the DRT The plant (Fig. 2) was described previously in Sect. 2.4 in the discussion of the StateTime toolset and in the description of the relay module (Fig. 3). The output object of the plant updates the pressure and power readings at most every two ticks of the clock. If the endupdate event is deleted with only the update object remaining, then pressure and power would be forced to change their values. With endupdate included, the sensor updates can be preempted thus leaving open the possibility that pressure or power (or both) remain unchanged for an additional two ticks. The output object for power and pressure updates could have been included in the con- troller as it represents the filtered sensor readings not the generation of power and pressure in the plant itself which are continuously changing. Since the output object behaviour is fixed and known a priori, it is more convenient to include it with the plant. In contrast to the plant, parts of the controller are initially unknown. It is known that there will be 3 microprocessors together with a majority voting circuit, i.e. the controller can be decomposed into sub-modules (Fig. 8) described by: FIGURE 8. Architecture of the controller based on majority voting control module controller in W, P /* power and pressure variables from the plant */ out C : {0,1} where /* relay activation variable based on majority vote. means send a signal to the relay to request it to open */ out : {fail, normal} where for /* failure variables needed for specifying failed behaviour */ out : {0,1} where for     /* means the j-th microprocessor is at or has returned to the beginning of a timing cycle where it waits for unsafe power or pressure signals*/ Body private : {0,1} where for /* The j-th microprocessor outputs a relay activation variable as input to the majority voting cir- cuit. The majority voter must decide, based on the microprocessor relay activation variables, whether to send an actual command to the relay of the plant via . The interconnection diagram between the modules of the controller is shown below: */ Specification : (Eq. 12) The formulas bothHi, powerHi and powerLo are defined in (Eq. 17). The module specification (Eq. 12) is similar to the DRT requirement R but with the controller output variable C playing the same role for the controller specification that the relay variable plays in R. The specification is stated under the proviso that at least two of the microprocessors work normally, as the majority voting logic is only robust with respect to a single failure. The last conjunct of the consequent asserts that the con- troller cycle is at most 52 ticks of the clock, after which it is guaranteed to be back at its initial posi- tion (it is not 50 ticks as it may take up to two ticks to detect a change in the plant). Since the environment of the controller is the (fixed) plant, the controller specification can be weakened to: (Eq. 13) (Eq. 12) end controller (Eq. 14) The microprocessors can either be in a normal or failed mode. The j-th microprocessor thus has an observable out variable with (Fig. 7). However, the precise nature of the normal behaviour is initially unknown, although the informal tim- ing diagram (Fig. 6) does provide some guidance. It is necessary to be able to tell when a microprocessor is at the initial point of a timing cycle where it checks for unsafe pressure and power levels (before invoking the two timers described in Fig. 6). Once a timing cycle is initiated in response to unsafe power or pres- sure levels, a new timing cycle cannot be initiated until the controller returns to its initial point. Hence, the j-th microprocessor also has an observable out variable with where means that the microprocessor is at its initial point. We require that a microprocessor timing cycle take no longer than the combination of the two timers which is 50 ticks with an additional two ticks to cover controller reaction times, i.e. . We are now in a position to state the DRT requirements for 3-version control. The informal requirements [R1] and [R2] can be stated in temporal logic for any two function- ing microprocessors and as: (Eq. 15)R1: (Eq. 16)R2: where the predicates bothHi, powerHi and powerLo are defined as: (Eq. 17) The controller can only react to changes in the pressure and power that persist long enough for the controller to be guaranteed to detect them (2 ticks of the clock). The con- troller microprocessors can sample pressure and power only once every tick of the clock. Hence, we require that the pressure and power both remain high for at least two ticks of the clock for the relay to open [R1]. Similar considerations apply when closing the relay [R2]. The requirements as stated above do not take into account the possibility of micropro- cessor failures. R1 and R2 can only be required to hold if at least two of the microproces- sors are functioning normally. The final requirement R is therefore: (Eq. 18)R: where the integer variables i and j range over the three microprocessor controllers, i.e. . 5.3 Problem to be solved We must prove that the DRT conforms to its requirements. Formally, this means we must prove that holds where and R is the formula given in (Eq. 18). Using the Composition Rule, a proof outline is: 1. modular-validity of (Eq. 5) in Fig. 2 for the plant by model-checking 2. modular-validity of (Eq. 12) in Fig. 8 for the controller by model-checking 3. general-validity (similar to the proof of (Eq. 8)) 4. 1, 2, 3 and the Composition Rule 5. The body of the plant module is given in Fig. 2. The only input variable to the plant is the relay activation variable , which can be altered arbitrarily by the environment transi- tion without generating too large a reachability graph. Hence step 1 in the above proof out- line was verified using StateTime model-checking. The only part of the above proof that cannot be verified is step 2, as the controller body is only partially defined at this point in the development. Thus we must complete the design of the controller by designing its body, and demonstrate the modular validity of the controller specification. Then the above proof outline guarantees that the DRT conforms to its requirements. In checking the modular-validity of the controller specification (Eq. 12), it is sufficient replace step 2 above with the weaker specification (Eq. 13). Instead of using an unre- stricted environment transition, (Th. 3) allows us to check sub-modules of the controller in the environment . The resultant reachability graphs of the sub-modules are much smaller than if an unrestricted environment transition is used. The above proof that the DRT conforms to its requirements then becomes: 1. modular-validity of the plant specification 2. modular-validity of (Eq. 13) in Fig. 8 for the controller 3. (Th. 1)(b) 4. 2,3 and temporal logic 5. general-validity via deductive theorem proving 6. 1, 4, 5 and the Composition Rule The design of the DRT controller will be performed using the structured compositional approach described by the structure diagram (Fig. 1) as outlined in the introduction. The structure diagram for the DRT is given in Fig. 9. FIGURE 9. Structure diagram for the DRT See Fig. 1 in the introduction for the interpretation of the structure diagram 5.4 Controller design A partial description of the controller was provided in Fig. 8. The majorityVote sub- module of the controller was described in Sect. 3.3 (Fig. 4). We must now design the microprocessor sub-modules. The body of the module is shown in Fig. 10, with the other two microprocessors having symmetric descriptions. FIGURE 10. Control module module micro1 in W,P /* power and pressure from the plant */ out : {0,1} where /* the fail variable */ out : {0,1} where /* relay activation variable*/ out : {0,1} where /* initial condition variable for start of timing cycle */ Body private where /* object variable of normal */ Specification: : where:    end module The normal object of the controller (Fig. 10) is a more thorough description of the infor- mal timing diagram of the analog controller (Fig. 6). The lower and upper time bounds of 1 in the transitions of normal indicate that the microprocessor samples the sensor inputs and passes through a block of control code every tick of the clock (0.1 seconds). Once unsafe power and pressure levels are detected by the transition mu, the normal object waits in activity n1 for 29 clock ticks (2.9 seconds) before proceeding to activity n2. If the power is still high then the relay activity variable is set via transition alpha, else the system resets via transition rho1. The second timer Timer2 of the analog controller is described by the delay20 transition. The beta transition resets the control activation variable when power returns to normal levels. It is obvious from the foregoing that TTMs can provide precise convenient descriptions of timing information. The normal object can be seen as a high level specification of the microprocessor. The microprocessors do not have delay and time-out constructs; rather, timing variables must be incremented every pass through the block of code to keep track of the passage of time. In Sect. 5.5, normal will be refined closer to code that can be imple- mented on the microprocessors. Once the body of the microprocessor module is known, the modular-validity of in Fig. 10 can then be verified via StateTime model-checking. As explained at the end of Sect. 5.3, the controller will be used in the constrained environment of the plant. Hence we need not consider an environment transition that can arbitrarily modify power and pressure. The output object of the plant (Fig. 2) allows updates of power and pressure at most once every two ticks of the clock; this constrained environment will produce a smaller reachability graph. Hence, instead of showing the modular-validity of (Eq. 12), we can verify the weaker validity (Eq. 13) given by by model checking . Since the microprocessor and majority vote modules satisfy their module specifica- tions, we can now show that is modularly-valid. Let be integer vari- ables that range over the three microprocessors (). Then 1. Assume 2. modular validity 3. modular validity of 4. 2,3 and the Composition Rule 5. 1, 4 and temporal logic (see Fig. 10 for the micro specifications ) 6. general-validity 7. integer reasoning 8. 1,5,6,7 and temporal logic 9. modular-validity of majorityVote module 10. 8,9 and the Composition Rule Line (10) of the above proof produces the first conjunct in the consequent of the controller specification (Eq. 12). The other conjuncts are obtained by similar (and much simpler) reasoning. We thus have: 11. discharging 1. 12. i and j were arbitrary; a constrained environment was used As shown in Sect. 5.3, the above result implies that the DRT conforms to its require- ments. The proof of conformance used a combination of model checking (for verifying modular-validity) and deduction (e.g. for proving the general validity in step 6). 5.5 Refining the controller The abstract module (Fig. 10) is observationally equivalent to its refinement (Fig. 11), i.e. . The refinement is closer to the final pseudocode [38]. As mentioned in Sect. 4.0, two methods have been developed for show- ing observational equivalence: FIGURE 11. Refinement of microprocessor control module /* Body of with same interface stub and module specification as (Fig. 10) €/ private Ta: {0 ... 30} where (Ta = 0) /* Timer1 variable in timing diagram */ private Tb: {0 ... 20} where (Tb = 0) /* Timer2 variable in timing diagram */ € The designer can interactively apply equivalence preserving transformations to derive from . The reader may consult [25] where this transformation is done for a TTM body the same as that of but without the additional failure transition and the initial condition variable . The proof used in [25] can be used as is for . The transformation rules can be applied to infinite state systems, but it can be shown that there is no complete set of transformations, i.e. there is no finite set of transformations such that it is always possible to prove TTM equivalence by using that set of transformations [27]. € For TTMs that can be reduced to finite state reachability graphs, there is an efficient polynomial time algorithm for showing observational equivalence [28]. The equiva- lence of and can be shown with this algorithm as the data types are finite. The abstract module satisfies the non-Zeno condition (Table 1). Since is SESI (state event stuttering invariant) over the interface variables, (Th. 4) guarantees that also holds for the refinement . Thus there is no need to redo the proofs of controller module specifications, and we remain with the guarantee that the DRT conforms to its requirements. The module is a high level description of a microprocessor controller. It is eas- ier to understand than because it is close to the informal timing diagram of the analog controller (Fig. 6). It does not have the two timer variables that has, and as a result the guards on its transitions are simplified relative to those of . Its reach- ability graph is smaller (Table 1). TABLE 1. Improved model checking times for the module compared to Modularly valid specifications Abstraction Refinement (Fig. 10) 13785 states in 26 seconds 59452 states in 297 seconds (non-Zeno constraint) 15248 states in 61 seconds 69059 states in 261 seconds Table 1 shows the result for checking the most complex module. However, all the mod- ule specifications were verified using the model-checker. The deductive parts of the proof were done by hand. In principal the deductive part could have been done using the theo- rem prover, but it proved too tedious as explained at the end of Sect. 2.4. We refer the reader to [38] for a discussion of the reverse engineering problem, i.e. how one goes from the pseudocode described in the original requirements document to the refinement presented in Fig. 11. 5.6 The design method Although top-down design by stepwise refinement was de rigueur until the 1980¹s, it has subsequently come under attack. As Jackson has written [20]: ³It was one thing to impose a single hierarchical structure on a sequential program of the programmer¹s own devising; it was quite another to impose it on a given, inconveniently ill-structured, real world domain². In fact, real-systems such as the DRT often have no single ³top² function. Our design method uses both top-down as well as bottom-up techniques. We have stressed in previous sections that the Composition and Refinement Rules can be used both ways. Our top-down methodology differs from the classic notion of stepwise refinement. In classic top-down design, a program is a single sequential process; concurrency and par- allelism was ³exotic² or unknown [20]. By contrast, TTM modules allows for nondeter- minism, and serial as well as parallel constructs in any mixture and to any depth. This allows for adequate descriptions of real systems that have no ³top² in the functional sense. Furthermore, at the top level, we do have requirements describing the safety and correct- ness of the overall system consisting of different parts (such as the plant and the control- ler). Such system requirements (e.g. the DRT requirements R1 and R2) are often emergent properties, i.e. they arise out of the combined interaction of the system modules taken together. There is thus still an urgent need to describe systems in a layered modular fash- ion, but without the sequential restrictions of the earlier methods. We now describe in outline the basic design method. The notions of a module, compo- sition and refinement developed in this paper, provide the precise theoretical underpin- nings for the method which was originally sketched in [36, pages 4-6]. We also borrow concepts from the insightful description of requirements in [20, p169]. The basic design procedure starts with requirements R. Requirements are about the phenomena of the application domain (the relay, pressure and power of the DRT plant), not about the machine (the controller). Our first step in requirements is to divide the sys- tem into the two parallel objects: (a) the plant which can be described as it already exists and (b) the controller which must be designed. This division proceeds by describing their relevant interfaces and connections, as well as some of the internal phenomena and entities of the plant ‹ this is the body of the plant which is a model of plant behaviour. The plant model cannot be too abstract because then it is not about the real problem anymore. It is a mistake to rush to the solution (by coding the controller) before delineating the problem to be solved (the plant requirements). The requirements are temporal logic formulas in plant entities such as pressure, power and the state of the relay. Therefore, the requirements do not describe the internal phenomena of the controller, although they might describe enti- ties at the boundary of the controller and the plant (the shared phenomena). It is the job of the controller to ensure that the requirements are satisfied, which it can do due to fact that it shares some phenomena with the plant (as described by the plant-con- troller interface). The controller might not be able to react to a shared phenomenon imme- diately (e.g. a change in reactor pressure), but the shared phenomenon happens in both the plant and controller simultaneously. Because the controller does not always know all the plant phenomena (or at least can- not react to them immediately), there is always the possibility of a gap between the requirements and what the controller can achieve (as described in the controller specifica- tion). The progression from requirements to controller implementation is a way of bridg- ing the gap between them. From the requirements expressed in terms of the plant, you derive a specification S of the controller in terms of the shared phenomena of the plant and controller. Then you derive the body of the controller from the controller specification. The Composition Rule justifies the eventual claim that the controller implementation satis- fies the requirements by reasoning as follows: (a) the body of the controller satisfies the specification S and (b) the specification S together with the description of the plant entails the truth of requirements R. In the case of the DRT controller, once the top-level interface stub was described, the parts of the controller were developed bottom-up component by component. A generic microprocessor controller was designed which was then instantiated three times to obtain 3-version control. Then the majority voting logic was designed. Bottom level modules were developed, simulated and verified to conform to their local specifications long before the modules were combined together. The plant description was quite simple and could be encapsulated in a single module. In more complicated application domains, the plant might also benefit from a bottom-up development. 6.0 Conclusions and related work This paper has presented a structured compositional method for the deliberate design of real-time systems, and applied the method to an industrial example with partial support provided by the StateTime toolset. The main novelty of the approach is to provide a fully compositional definition of real-time reactive modules compatible with existing model- checking tools (Sect. 3.0) and a refinement relation (Sect. 4.0). This allows for the system- atic development and verification of real-time systems. There are four main areas where mechanical support is needed: (1) system simulation for validating models, (2) model-checking for modular-validity, (2) deductive theorem proving for the composition rule, and (3) proving observational equivalence for the refine- ment rule. StateTime was used for simulation and model-checking all module specifications of the DRT example. Although, in principal, we could have used the toolset for the deductive part, it proved too unwieldy due to the proliferation of quantifiers. The toolset has no sup- port for refinement, and this had to be done by hand using behaviour preserving transfor- mations. So too, there is a need to directly supports modules with interface stubs and automatic generation of environments. This leads us to the main conclusion of this paper. StateTime, as it currently stands, needs to be enhanced in a variety of ways if it is to support more seamless compositional verification. I am therefore currently working, together with Lewis Lo, on a new version of StateTime that builds on the reactive modules introduced in this paper, and allows for the complete spectrum of automated simulation, model-checking and theorem proving tools. The enhanced StateTime will also support modules (interface stubs and automatic gen- eration of environments). We use count-up and count-down clock variables with ordinary temporal logic (rather than the bounded operators of RTTL) for specification, but it is yet to early to tell to what extent this will simplify deductive reasoning. The proof of observation equivalence (both algorithmically for finite state modules and via equivalence preserving transformations) for use in the refinement rule needs to be implemented and incorporated into the StateTime toolset, but we have not yet decided how to implement these techniques. Because our bisimulation relation involves both states and events (Sect. 4.0), we may not be able to directly use existing tools such as Concurrency Workbench [9]. The Concurrency Workbench allows for the testing of equivalences and preorders and the verification of systems in the modal mu-calculus; real-time CCS style front-ends are available. Other tools such as Modechart [21], Statemate [16] and ObjectTime [45] also use state- charts for visual system descriptions. Modechart allows for both simulation and algorith- mic analysis techniques for a subset of properties expressed in a predicate real-time logic [34]. Statemate can be used to do reachability analysis and ObjectTime is object-oriented which is useful in design, but it cannot deal with hard real-time systems. None of these tools have theorem provers, nor do they allow for modular verification. RTTL is based on the linear time temporal logic LTL rather than on branching time log- ics such as CTL. It is commonly accepted that while specifying is easier in LTL, model- checking is more efficient in CTL. Both linear and branching time languages now have efficient model-checkers using either partial orders or BDD methods: SPIN [18] is one of the few LTL based model-checkers. SMV is a good example of a CTL based model- checker [5], with an extension to real-time systems called Verus which uses a branching time real-time language called RTCTL [6]. Verus also has the facility for specifying task priorities. The hybrid tool HyTech [2] extends branching time model-checking to continu- ous real-time systems using stop watches and symbolic fixpoint computation (the current version of the tool supports reachability analysis via monitor automatons and not directly the full set of CTL formulas). HyTech and Verus both allow for parametric analysis (e.g. determining the latest possible moment a controller can wait before issuing a command). The STeP [31] model-checker and theorem prover was chosen as the back-end to StateTime rather than tools such as SPIN, SMV and HyTech for a number of reasons. Tools that use a non-interleaving synchronous execution step algorithm (e.g. SMV, the PVS model-checker [42] and COSPAN [15]) are efficient for dealing with hardware designs, but do not seem to be as efficient as SPIN when it comes to dealing with inter- leaved sequential code and integer variables. There is also another problem associated with modularity when it comes to branching time model-checkers. Although branching time is usually more efficient than linear time logics, the branching time algorithms become EXPTIME-complete for module checking which is worse than the PSPACE com- plexity of linear time logics [24]. This analysis seems to suggest that the accepted trade-off between LTL and CTL for modules is not as simple as it is for closed systems. We were not able to use SPIN because it only supports justice (weak fairness) not compassion (strong fairness) needed for the tick transition. More importantly, we hope to use the theo- rem proving components of STeP in future versions of our tool. None of the aforemen- tioned tools (except PVS) have theorem provers. Hooman [19] extends Hoare logic to real-time programs by freely mixing programs and assumption/guarantee assertions leading to a top-down derivation method. The theory is implemented using the interactive proof checker PVS [42]. The embedding of the proof system in PVS provides powerful mechanical support for compositional reasoning (but not model checking). The only timing construct is the precise delay; there are no time bounds on transitions as in TTMs. There is a growing interest in compositional and refinement methods for reactive sys- tems [1,7,22,35,41,46,48]. The field is somewhat less developed in the case of real-time systems especially in methods that also have tool support. ASTRAL [10] is based on the framework of [11] that uses Petri Nets for system descriptions and a timed temporal logic called TRIO for specifications. ASTRAL provides structuring mechanisms that allow the designer to build modularized specifications that are translated into TRIO. Proofs in ASTRAL are either interlevel or intralevel. The former deals with proving that the specification at a higher level is consistent with a specification at a lower level. The latter deals with proving that a description at a level satisfies its spec- ification. A tool is currently under development. The frameworks mentioned thus far have specification languages that are based on logic, usually modal logic. Other approaches are based on algebra or automata. Discrete real-time process algebras [4,44] can describe systems compositionally at different levels of abstraction. The semantics of process algebras is usually defined in terms of labelled transition systems. An algorithm based on observation (bisimulation) equivalence is used to show that an implementation satisfies its specification. These bisimulation relations are usually event-based [33], whereas the bisimulation relation used in this paper is both event and state-based (Sect. 4.1). It is event-based in order to ensure a global notion of time via the tick transition. It is state-based so that module specifications can be written as temporal logic properties in the observable variables. Continuous time extensions to process alge- bras [47] lack the abstracting power of a congruence relation of the discrete event case, due to technical difficulties associated with their infinite branching continuous time semantics. The real-time CSR language [13] provides a layered approach to dealing with shared resources. [12] presents hierarchical multistate machines for multilevel specifications. The automata based tool COSPAN has recently been extended to deal with real-time [3]. COSPAN supports top-down development through successive refinements and homomor- phic reduction [15]. Timed automata [30] (see also the input/output automata described in [29]) have visible actions, a time passage action (analogous to our clock tick) and a special internal action. Dense upper bounds can be imposed between actions, but not lower time bounds. A refinement from one timed automaton to another is a time-preserving function similar to the classical notion of a homomorphism between automata. In single language frameworks (e.g. automata based COSPAN or the logic based TLA [1]), both the implementation and specification are expressed in the same formalism (automata or logic). Conformance is proved by demonstrating that each fair trace of the implementation is also a fair trace of the specification. There is a certain elegance and sim- plicity associated with using a single language for both specifications and implementa- tions. We have pursued the dual TTM/RTTL framework in this paper as it provides us with the flexibility of using the most appropriate analysis technique in each case. For TTM refinement, we use the algebraic notion of observation equivalence, and for TTM compo- sition the logical conjunction of RTTL specifications. Acknowledgments I would like to thank Mark Lawford for his help with all aspects of this paper. I also thank the anonymous referees for their helpful criticisms, comments and suggestions. 7.0 References [1] Abadi, M. and L. Lamport. ³Conjoining Specifications.² ACM Trans. on Programming Languages and Systems, 17(3): 507-534, 1995. [2] Alur, R., T.A. Henzinger, and P.-H. Ho. ³Automatic Symbolic Verification of Embedded Systems.² IEEE Transactions on Software Engineering, 22(3): 181-201, 1996. [3] Alur, R. and R.P. Kurshan. ³Timing Analysis with Cospan.² In Hybrid Systems III, ed. R. Alur, T.A. Henzinger, and E. Sontag. LNCS 1066 Springer Verlag, 1996. [4] Baeten, J.C.M. and J.A. Bergstra. ³Discrete Time Process Algebra.² Formal Aspects of Computing, 8(2): 188-208, 1996. [5] Burch, J.R., E.M. Clarke, K.L. MacMillan, D.L. Dill, and L.J. Hwang. ³Symbolic Model Checking: 10^20 States and Beyond.² Information and Computation, 98(2): 142-170, 1992. [6] Campos, S.V. and E.M. Clark. ³ Real-Time Symbolic Model Checking for Discrete Time Models.² In Theories and Experiences for Real-Time System Development, ed. T. Rus and C. Rattray. AMAST Series in Computing, Vol. 2. World Scientific Press, 1994. [7] Chandy, K.M. and J. Misra. Parallel Program Design. Addison-Wesley, 1988. [8] Chang, E. ³Compositional Verification of Reactive and Real-Time Systems.² Ph.D, Stanford University, 1995. [9] Cleaveland, R. and S. Sims. ³The NCSU Concurrency Workbench.² In Computer-Aided Verification (CAV '96), New Brunswick, NJ, edited by R. Alur and T. Henzinger, Springer-Verlag, LNCS 1102, 394- 397, 1996. [10] Coen-Porisini, A., R. Kemmerer, and D. Mandrioli. ³A formal framework for ASTRAL intralevel proof obligations.² IEEE Transactions on Software Engineering, 20(8): 548-560, 1994. [11] Felder, M., D. Mandrioli, and A. Morzenti. ³Proving properties of real-time systems through logical specifications and Petri Net models.² IEEE Transactions on Software Engineering, 20(2): 127-141, 1994. [12] Gabrielian, A. and M. Franklin. ³Multilevel specifications of real-time systems.² Communications of the ACM, 34(5): 51-60, 1991. [13] Gerber, R. and I. Lee. ³A layered approach to automating the verification of real-time systems.² IEEE Transactions on Software Engineering, 18(9): 768-784, 1992. [14] Gries, D. and F.B. Schneider. A Logical Approach to Discrete Math. Springer Verlag, 1993. [15] Hardin, R.H., Z. Harel, and R.P. Kurshan. ³COSPAN.² In 8th International Conference on Computer Aided Verification CAV'96, LNCS 1102 Springer-Verlag, 421-427, 1996. [16] Harel, D., H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, and M. Trachtenbrot. ³Statemate: a working Environment for the Development of Complex Reactive Systems.² IEEE Transactions on Software Engineering, 16:403­414, 1990. [17] Harel, D. and A. Pnueli. ³On the Development of Reactive Systems.² In Logics and Models of Concur- rent Systems, ed. K. Apt. 477-498. F-13 of NATO Advanced Summer Institutes. Springer-Verlag, 1985. [18] Holzmann, G. ³The Model Checker Spin.² IEEE Trans. on Software Engineering, 23(5): 279-295, 1997. [19] Hooman, J. ³Correctness of Real-Time Systems by Construction.² In Proc. Symposium on Formal tech- niques in Real-Time and Fault-Tolerant Systems, 19-40. LNCS 863 Springer-Verlag, 1994. [20] Jackson, M. Software Requirements & Specifications. Addison-Wesley, 1995. [21] Jahanian, F. and A.K. Mok. ³Modechart: A Specification Language for Real-Time Systems.² IEEE Transactions on Software Engineering, 20(12): 933-947, 1994. [22] Jones, C.B. ³Specification and design of parallel programs.² In IFIP 9th World Congress, 321-323, 1983. [23] Kesten, Y., Z. Manna, and A. Pnueli. ³Verifying Clocked Transition Systems.² In Hybrid Systems III, Springer-Verlag, LNCS, 1996. [24] Kupferman, O. and M.Y. Vardi. ³Module Checking.² In 8th International Conference on Computer Aided Verification CAV'96, LNCS 1102 Springer-Verlag, 75-86, 1996. [25] Lawford, M. ³Transformational Equivalence of Timed Transition Models.² Systems Control Group, Department of Electrical Engineering, University of Toronto. TR-9202 (M.A.Sc. thesis), 1992. [26] Lawford, M., J.S. Ostroff, and W.M. Wonham. ³Model Reduction of Modules for State-Event Temporal Logics.² In IFIP Joint International Conference on Formal Description Techniques (FORTE-PSTV'96), Chapman & Hall, 1996. [27] Lawford, M. and W.M. Wonham. ³Equivalence Preserving Transformations for Timed Transition Mod- els.² IEEE Trans. on Automatic Control, 40(7): 1167-1179, 1995. [28] Lawford, M., W.M. Wonham, and J.S. Ostroff. ³State-Event Labels for Labelled Transition Systems.² In Proc. 33rd IEEE Conference on Decision and Control, Orlando, FL, IEEE Control System Society, 3642-3648, 1994. [29] Lynch, N. and R. Segala. ³A Comparison of Simulation Techniques and Algebraic Techniques for Ver- ifying Concurrent Systems.² Formal Aspects of Computing, 7(3): 231-265, 1995. [30] Lynch, N. and F. Vaandrager. ³Forward and Backward Simulations for Timing-Based Systems.² In REX Workshop ‹ Real-Time: Theory in Practice, 397-446. LNCS 600 Springer-Verlag, 1992. [31] Manna, Z. ³STeP: The Stanford Temporal Prover.² Dep. of Computer Science, Stanford University. STAN-CS-TR-94-1518, 1994. [32] Manna, Z. and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, New York, 1992. [33] Milner, R. Communication and Concurrency. Prentice Hall, 1989. [34] Mok, A. and D. Stuart. ³Simulation vs. Verification: Getting the Best of Both Worlds.² In 11th Annual IEEE Conference on Computer Assurance (COMPASS), Washington D.C, 1995. [35] Mokkedem, A. and D. Mery. ³On Using Temporal Logic for Refinement and Compositional Verifica- tion of Concurrent Systems.² Theoretical Computer Science, 140:95-138, 1995. [36] Ostroff, J.S. Temporal Logic for Real-Time Systems. Advanced Software Development Series, ed. J. Kramer. Research Studies Press Limited (distributed by John Wiley and Sons), England, 1989. [37] Ostroff, J.S. ³Deciding properties of Timed Transition Models.² IEEE Transactions on Parallel and Distributed Systems, 1(2): 170-183, 1990. [38] Ostroff, J.S. ³A Visual Toolset for the Design of Real-Time Discrete Event Systems.² IEEE Trans. on Control Systems Technology, 5(3): 320-337, 1997. [39] Ostroff, J.S. and H.K. Ng. ³The Design of Real-Time Systems Using Standard Untimed Theories.² In Preprints Third AMAST Workshop on Real-Time Systems, Salt Lake City, Utah, ONR and Iowa Univer- sity, 1996. [40] Ostroff, J.S. and W.M. Wonham. ³A Framework for Real-Time Discrete Event Control.² IEEE Transac- tions on Automatic Control, 35(4): 386­397, 1990. [41] Owicki, S. and D. Gries. ³Verifying properties of parallel programs: an axiomatic approach.² Communi- cations of the ACM, 19(5): 279-285, 1976. [42] Owre, S., J. Rushby, N. Shankar, and F.v. Henke. ³Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS.² IEEE Trans. on Software Engineering, 21(2): 107-125, 1995. [43] Parnas, D.L., G.J.K. Asmis, and J. Madey. ³Assessment of Safety-Critical Software in Nuclear Power Plants.² Nuclear Safety, 32(2): 189-198, 1991. [44] Schneider, S., J. Davies, D.M. Jackson, G.M. Reed, J.N. Reed, and A.W. Roscoe. ³Timed CSP: Theory and Practice.² In REX Workshop --- Real-Time: Theory in Practice, 640-675. LNCS 600, Springer-Ver- lag, 1992. [45] Selic, B., G. Gullekson, J. McGee, and I. Engelberg. ³ROOM: An Object-Oriented Methodology for Developing Real-Time Systems.² In CASE¹92 Fifth International Workshop on Computer-Aided Soft- ware Engineering, Montreal, IEEE Computer Society Press, 230-240, 1992. [46] Stolen, K., F. Dederichs, and R. Weber. ³Specification and refinmenent of networks of asynchronously communicating agents using the assumption/commitment paradigm.² Formal Aspects of Computing, 8(2): 127-161, 1996. [47] Yi, W. ³CCS + Time = an Interleaving Model for Real Time Systems.² In Proceedings of ICALP'91, 217-228. LNCS 510 Springer-Verlag, 1991. [48] Zwiers, J. and W.P.d. Roever. ³Compositionality and modularity in process specification and design.² In Temporal logic in specification, ed. B. Banieqbal, H. Barringer, and A. Pnueli. 351-374. LNCS 398 Springer-Verlag, 1989.