844

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,

VOL. 34,

NO. 6,NOVEMBER/DECEMBER 2008

Timed Automata Patterns
Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, and Wang Yi
Abstract—Timed Automata have proven to be useful for specification and verification of real-time systems. System design using
Timed Automata relies on explicit manipulation of clock variables. A number of automated analyzers for Timed Automata have beendeveloped. However, Timed Automata lack composable patterns for high-level system design. Specification languages like Timed
Communicating Sequential Process (CSP) and Timed Communicating Object-Z (TCOZ) are well suited for presenting compositionalmodels of complex real-time systems. In this work, we define a set of composable Timed Automata patterns based on hierarchicalconstructs in time-enriched process algebras. The patterns facilitate the hierarchical design of complex systems using Timed
Automata. They also allow a systematic translation from Timed CSP/TCOZ models to Timed Automata so that analyzers for Timed
Automata can be used to reason about TCOZ models. A prototype has been developed to support system design using Timed
Automata patterns or, if given a TCOZ specification, to automate the translation from TCOZ to Timed Automata.
Index Terms—Timed Automata, timed patterns, TCOZ, UPPAAL.

Ç1

INTRODUCTIONS

PECIFICATION andverification of real-time systems areimportant research topics that have practical implications. A popular approach for specifying real-time systems
relies on the graphical notation Timed Automata [2], [35].
Timed Automata are powerful in designing real-time models
with explicit clock variables. Real-time constraints arecaptured by explicitly setting/resetting clock variables. A
number of mechanized verification support for Timed
Automata have proven to be successful (e.g., UPPAAL,KRONOS, TEMPO, RED, and Timed COSPAN). However,designing and verifying real-time systems is becoming an
increasingly difficult task due to the widespread applications
and increasing complexity of such systems. High-level
requirements for real-time systems are often stated in terms
like deadline, time-out, and wait until, partly evidenced by thecase studies presented in [31], [16], [13], [34], [19]. In industrial
case studies of real-time system verification, system requirements are often structured into phases, which are thencomposed sequentially, in parallel, alternatively, etc. [25],[32]. Unlike Statechart or process algebras, Timed Automata
lack high-level composable patterns (besides parallel composition) for hierarchical design. Timed Automata users often
need to manually cast those terms into a set of clock variables
with carefully calculated clock constraints. The process istedious and error prone.

. J.S. Dong, P. Hao, and J. Sun are with the School of Computing, National
University of Singapore, 3 Science Drive 2, Singapore 117543, Republic ofSingapore. E-mail: {dongjs, haoping, sunj}@comp.nus.edu.sg.
. S. Qin is with the Department of Computer Science, Durham University,
Science Laboratories, South Road, Durham DH1 3LE, UK.
E-mail: shengchao.qin@durham.ac.uk.
. W. Yi is with the School of Scince and Engineering, North Eastern
University, P.R. China ans the Department of Information Technology,
Uppsala University, Box 337,751 05, Uppsala, Sweden.
E-mail: yi@it.uu.se.
Manuscript received 10 Aug. 2007; revised 12 May 2008; accepted 19 June
2008; published online 23 July 2008.
Recommended for acceptance by R. Cleaveland.
For information on obtaining reprints of this article, please send e-mail to:
tse@computer.org, and reference IEEECS Log Number TSE-2007-08-0239.
Digital Object Identifier no. 10.1109/TSE.2008.52.
0098-5589/08/$25.00 ß 2008 IEEE

Process algebras, on the other hand, are known for theirbottom-up composibility, which is important to fight against
the complexity of the system design. In the literature, anumber of language-based process algebras have proven to
be useful for specifying complex hierarchical real-timesystems. Timed Communicating Sequential Processes(Timed CSPs [40]), which extend the classic CSP [27], support
a rich set of compositional constructs to capture system
requirements, e.g., time-out, timed interrupt, timed-event
prefixing, etc. Together with compositional constructs likeexternal/nondeterministic choice, recursion, and interrupt,
Timed CSP offers a powerful mechanism for designingcomplex real-time systems. Timed Communicating Object-Z(TCOZ [36]) is an integrated high-level formal specification
language that builds on the strengths of Timed CSP andcombines it with Object-Z (OZ) [17] for modeling data andfunctional aspects of complex systems. In addition, newcompositional constructs have been introduced, e.g., deadline and wait until. The downside of being expressive is that it
is highly nontrivial to mechanically validate TCOZ models.
For safety-critical systems, exposing a possible violation ofsystem requirements at the specification level is very
important, especially for hard timing constraints. The
challenge of verifying time-enriched process algebras haslong been recognized. A model checker named FDR [39] hasbeen developed to verify CSP. However, there is nosatisfactory verification support for either Timed CSP or
TCOZ.
Based on the time-proven compositional constructs inTimed CSP/TCOZ, we develop a set of composable time
patterns for Timed Automata which facilitates high-levelsystem design using Timed Automata. The patterns cover alarge class of common real-time behavior patterns and yet
can be composed to form new useful patterns. The patterns
are formally defined. By following the formal semantics(which are originated from their images in time-enriched
process algebras), a high-level design composed of multiple
timed patterns can be flattened to ordinary Timed Automata automatically. Thus, existing tools like UPPAAL canbe used to verify time patterns with little computational
overhead. On the other hand, the patterns allow a
Published by the IEEE Computer Society

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

DONG ET AL.: TIMED AUTOMATA PATTERNS

systematic translation from Timed CSP/TCOZ models to
Timed Automata so that the state-of-art verification
mechanism for Timed Automata can be used to validate
Timed CSP/TCOZ models.
This work identifies the strengths and weaknesses ofTimed Automata and timed process algebras and develops
new techniques for system modeling, as well as verification.
Instead of comparing the expressiveness of the two
notations (which is of theoretical interest and has been
partially done in [38]), we focus on developing practicaltechniques that are beneficial to both TCOZ/Timed CSP
and Timed Automata users. A closely related work is thehierarchical Timed Automata proposed in [11]. The notionof hierarchical Timed Automata in [11] is based the notionof Statechart. Two kinds of Timed Automata composition
have been discussed, i.e., named and-states and or-states. In
our work, the common time patterns introduced in Timed
CSP and beyond have been formally defined, which serve
as a library of building blocks for complex real-timesystems. This work is also related to works on verificationof time-enriched process algebra. In [15], Dong et al. havedeveloped a model checker for Timed CSP based on
constraint solving. In Brooke’s PhD dissertation [8], apreliminary PVS encoding of Timed CSP was presented
which relies heavily on user interaction. Another closely
related area of research is Hoenicke and Olderog’s work on
the integration of CSP, OZ, and Duration Calculus (DC)(named CSP-OZ-DC [28]). By transforming the DC part of asystem model into a Timed Automaton, CSP-OZ-DC
benefits from Timed Automata’s tool support. For instance,
UPPAAL has been used to verify CSP-OZ-DC models. In
our work, UPPAAL is used to verify TCOZ models.
However, our main contribution is the development of thegeneric Timed Automata patterns, i.e., we not only borrow
Timed Automata’s tool support for TCOZ verification but
also lend TCOZ’s hierarchical constructs to facilitate
systematic Timed Automata designs. Furthermore, thework in [28] mainly focuses on the smooth integration of
the underlying semantic models of CSP, OZ, and DC and its
use for verifying properties of CSP-OZ-DC specifications.
Another related formalism for modeling real-time systems
is TRIO [20]. This notation uses a notion of interface
diagram that is different from the Timed-CSP-featured
TCOZ notation in modeling dynamic behaviors. TRIO has
been compared to TCOZ [36]. Similar to our work, someother real-time formalisms have been translated or projected to other formalisms for model-checking [29], [23].
This work is also related to works on compositionalmodeling of real-time systems [4], [3], [41], [22] and works
on specification patterns in general [18], [30].
This paper is a revised and extended version of ourconference paper [14], in which the link between Timed
Automata and TCOZ has been investigated. A few timed
patterns have been briefly introduced to show our initialideas of reusing Timed Automata’s tool support to verify
TCOZ models. This paper substantially extends [14] with arange of common timed patterns, as well as a formaltransition from TCOZ to Timed Automata and its correctness proof. We further enhance our previous work with
illustrative examples, as well as a complex case study,
which demonstrate the applicability of our approach. The
remainder of the paper is organized as follows: Section 2
briefly introduces the relevant features of TCOZ and Timed

845

Automata. Section 3 presents our main contribution, i.e., a
set of composable Timed Automata patterns with formal
semantics. We also demonstrate how new patterns can becomposed from the existing ones. Section 4 shows how
TCOZ or Timed CSP users may benefit from our patterns,
by defining a formal translation from TCOZ to Timed
Automata. A JAVA application for automating the projection is briefly discussed. Section 5 shows how Timed
Automata users benefit from the patterns. We demonstratea hierarchical Timed Automata design using a railcar
system. Section 6 concludes this work. Throughout the
paper, a process means a TCOZ or Timed CSP process andautomata refer to Timed Automata unless otherwise stated.

2

BACKGROUND

2.1 Timed Automata
Timed Automata were proposed in [2] as an extension of
the automata-theoretic approach to the modeling of realtime systems. Since then, the theory and verification tool
support of Timed Automata has been an intensive field of
research in computer science. A Timed Automaton is a
finite automaton equipped with a finite set of clocks. Clocks
are continuous real-valued functions of time that precisely
record the time elapsed. All clocks advance at the samepace. Real-time system behaviors are captured using Timed
Automata by explicitly resetting clocks and comparing aclock reading with constants.
Definition 1 (Timed Automaton). A Timed Automaton A is a
7-tuple ðS; init; F ; ; C; Inv; T Þ, where S is a finite set ofstates, init 2 S is an initial state,1 F  S is a set of final
states,  is a set of actions/events, C is a finite set of clocks,
Inv is a proposition assignment function that, for each state,
gives a proposition true at the state, and T : S    2C ðCÞ  S is the transition relation. A transition ðs; a; ; ; s0 Þ
represents a transition from state s to state s0 on event a. The set 
gives the clocks to be reset with this transition and  is a clock
constraint over C that specifies when the switch is enabled. ðCÞis a set of clock constraints that is defined by the following
grammar: ’ :¼ truejx  cjc  xjx < cjc < xj’1 ^ ’2 , where
x is a clock and c is a real number.
Note that F might be empty if the Timed Automata neverterminates (i.e., no deadlock state). The semantics of a Timed
Automaton is defined as a transition system. A run of thetimed automaton starts with the initial state. The control may
remain at a state s as long as the state InvðsÞ is not violated. A
transition ðs; a; ; ; s0 Þ is enabled if and only if the control is atstate s, the guard condition  is satisfied (by the valuation of
the clocks), and the event a is enabled. The transition is
unguarded if  is true. After taking the transition, the control
moves to state s0 and the clocks in  reset.
Example. The following shows a sample Timed Automaton
specifying a railcar door (the railcar system will be
specified in Section 5).
1. If there were multiple initial states, a unique initial state is created withinternal transitions to the ordinary initial states.

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

846

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,

For the sake of readability, the states are labeled withnames, e.g., Open, Close, and T oOpen. We assume thatthe door can be closed instantly and, hence, there is nostate named T oClose. Initially, the control is at state
Close, indicated by the double-lined circle. The transitionis fired once an input is received over channel open (asthe transition is unguarded), the control goes to state
T oOpen, and clock x is reset. Within 2 seconds(constrained by the state invariant), the control goes tostate Open. An output on the channel conf takes place
along with the transition. The door remains open for
10 seconds, i.e., passengers have 10 time units forboarding, and, then, the control goes to state Close.
A Timed Automata specification may consist of a
network of Timed Automata. A state in the product of
two Timed Automata is a pair of states, each representing
the progress one of the Timed Automata has made so far. A
transition in the product is either a local transition of either
automaton or a synchronization between the two components. The synchronization is locking; for an input andoutput pair, a component can input/output if and only if
the other component can output/input. The following
formally defines the parallel composition. For simplicity,
we assume that there are no common clock variables. Notethat parallel composition is the only Timed Automata
pattern in the original proposal of Timed Automata [2].
Definition 2 (Parallel Composition). Let Ai ¼
ðSi ; initi ; Fi ; i ; Ci ; Invi ; Ti Þ where i 2 f1; 2g be two Timed
Automata. The parallel composition of A1 and A2 isparaðA1 ; A2 Þ ¼ ðS1  S2 ; ðinit1 ; init2 Þ; F1  F2 ; 1 [ 2 ;C1 [ C2 ; Inv; T Þ;
where
8ðs1 ; s2 Þ : S1  S2  Invððs1 ; s2 ÞÞ ¼ Inv1 ðs1 Þ ^Inv2 ðs2 Þ and T is the smallest transition relation satisfying
the following conditions:2
If ðs; a; ; ; s0 Þ 2 Ti ^ a 62 3i where i 2 f1; 2g, thenððs; tÞ; a; ; ; ðs0 ; tÞÞ 2 T .
. If ðs1 ; a; ; ; s2 Þ 2 Ti and ðs01 ; a; 0 ; 0 ; s02 Þ 2 T3i ,then ððs1 ; s01 Þ; a;  [ 0 ;  ^ 0 ; ðs2 ; s02 ÞÞ 2 T .
The indexed parallel composition of multiple automata is
written as paraðA1 ; A2 ; . . . ; An Þ, where A1 ; . . . ; An are timed
automata.
.

By definition, parallel composition is communicative anddistributive tracewise. A number of Timed Automata
verifiers based on the model checking technique have beendeveloped. In this work, we focus on the popular UPPAAL[33]. UPPAAL is a tool for the modeling, simulation, andverification of real-time systems. It consists of three mainparts: a system editor, a simulator, and a model checker.
The system editor provides a graphical interface for the tool.
2. In UPPAAL, a pair of input and output results in a silent transition.
Synchronization among multiple parties is mimicked using the notion ofcommitted states.

VOL. 34,

NO. 6,NOVEMBER/DECEMBER 2008

Typically, a system description consists of a set of instancesof Timed Automata declared from process templates and ofsome global data, such as global clocks, variables, andsynchronization channels. The simulator is a validation toolthat enables the examination of possible dynamic executions of a system. The model checker verifies invariants andbounded liveness properties by exploring the symbolic state
space of a system, i.e., reachability analysis in terms ofsymbolic states represented by constraints. The model
checking engine of UPPAAL is designed to check a
restricted subset of Timed CTL [1] formulas for networksof Timed Automata. Note that Timed Automata in
UPPAAL extend the original one [2] with handy constructs
like urgent states and committed states. No time elapsing isallowed at an urgent state, i.e., an urgent state is labeledwith an additional invariant that the control cannot reside at
the state. We write ðs; urgentÞ 2 Inv to mean that state s isurgent. In the following, states in the timed patterns may bemarked as urgent states so as to make it easier to prove thesoundness of the patterns and to simplify the flattened
Timed Automata (see later examples). An urgent state is
drawn as a circle with a “U” inside.

2.2 Time Communicating Object Z
A number of time-enriched process algebras have been
proposed. In this work, we focus on TCOZ [36], which,compared to others, contains a larger set of compositional
constructs. TCOZ is designed to present a complete andcoherent specification of systems with not only complicatedcontrol flows but also complex data and functional requirements. It is essentially a blending of OZ with Timed CSP, forthe most part preserving them as proper sublanguages of theblended notation. TCOZ is novel in that it includes timing
primitives, properly separates process control and data/
algorithm issues, fully integrates notions of refinement fromboth languages, supports the modeling of true multithreaded
concurrency, and distinguishes the notion of active andpassive objects. In the following, we walk through the mainfeatures of TCOZ using an illustrative example. A detailed
introduction to TCOZ and its Timed CSP and OZ features
may be found in [36].
Example. Fig. 1 presents a TCOZ specification of a timed
message queue. It contains a single class named
T imedQueue. The anonymous schema called state schema
identifies the data space of the class. In particular, thevariable item is a sequence of messages. MSG is an
uninterpreted data type. in and out of reserved typechan identifies the communication interfaces of thisclass, i.e., in and out are channels connecting objects ofthis class to its environment. Channels that share thesame base name in different classes are connected
implicitly. Tl , Tj , and To are time constants which areused to constrain the duration of a data operation. The
schema named INIT contains the predicate that identifies
the initial data state, i.e., items is empty. The two
schemas Add and Del are operation schemas. They define
the data operations that may update the valuation of thedata variables. The predicate part of an operation (the part
under the horizontal line) specifies an operation using a
predicate composed of primed and unprimed versions of
the data variables, as well as inputs/outputs. The primed
variables denote the valuation of the variable after theoperation. In particular, the predicate part of operation

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

DONG ET AL.: TIMED AUTOMATA PATTERNS

847

Fig. 1. Timed message queue specification.

Add means that the sequence of messages after theoperation should be the original sequence of messages
followed with the input. The remaining part is a set ofprocess definitions which specifies the dynamic behaviorof objects of this class. A process is defined by anequation. The left-hand side is the process name, e.g.,Join, Leave, and Main. Note that ¼
b means “is definedas.” The right-hand side is the process expression thatdefines the process. For instance, process Join behaves
as follows: after getting an input i from channel in (thepart ½i : MSG is a guard condition saying that i must beof type MSG), the operation Add is performed within
Tj time units (constrained by the DEADLINE expression).
The Leave operation specifies that if the sequence items
is not empty ðitems 6¼ ;Þ, the first element in itemsðheadðitemsÞÞ shall be sent over channel out and, then,operation Del is performed to remove this element fromitems in Tl time units. The process named MAIN
identifies the behavior of instances of the class after
initialization. In particular, the Main process is defined
as a recursion (as a  function). The process construct tumeans choice and .fTo g means time-out. The process
reads as “the system may either behave as prescribed by
Join or Leave or, if nothing happens in To time units,then the system performs operation Del in Tl time units
and then repeats from the beginning.” If no input or
output is performed in To time units, then the firstmessage is lost.
In this work, we focus on the process aspects of TCOZ,
which borrows and extends the modeling power of Timed
CSP. Table 1 shows a list of process constructs in TCOZ.
STOP denotes a process that deadlocks and does nothing.
SKIP denotes a process that terminates successfully. Process
WAIT t delays the system for exactly t time units. Process

e ! P is initially willing to engage in event e and behaves
as P afterward. A process e@t ! P ðtÞ behaves just like e !
P except that the engage time of e is recorded in t. The
event e can be a channel communication of the form c!a orc?a. In order to capture timing requirements naturally,
TCOZ supports common timing constraints like deadline
and wait until. Process P  DEADLINE t is constrained toterminate within t time units. The WAITUNTIL operator is adual to DEADLINE. Process P  WAITUNTIL t behaves as P
but will not terminate before t time units elapse. If P
terminates early, it idles until t time units elapse. Processes
may be compositional. The sequential composition P ; Q
behaves as P until it terminates and then behaves as Q. An
external choice is written as P t
u Q. Often, external choices
are guarded by prefixing or conditionals. The internal
choice P u Q behaves as either P or Q nondeterministically.
The parallel composition of two processes is written as
P j½EjQ, where E is a set of events. Events in E are
synchronized by P and Q. If E is the empty set, the twoprocesses interleave, written as P kjQ. Process P . ftgQ
behaves as P if P makes a move before t time units elapse;
otherwise, Q takes control. P 4 e ! Q behaves as P until
event e is engaged and, then, P is interrupted and Q takes
control. Process P 4 ftgQ is called timed interrupt. It
behaves as P until t time units elapse and then switches
to Q. Both interruptions are preemptive. Recursion isdefined as a  function. The semantics of recursion isdefined as Tarski’s weakest fixed point. It is known that
unbounded recursion in CSP (and, therefore, Timed CSP
and TCOZ) may result in irregular languages. Therefore, we
restrict ourselves to tail recursion, i.e., a special case ofrecursion in which only the last operation of a process is arecursive call.

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

848

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,TABLE 1Time-Enriched Process Constructs

VOL. 34,

NO. 6,NOVEMBER/DECEMBER 2008

represented as two triangles that are side by side. In thefollowing,  denotes an internal unobservable transition.
For simplicity, a function/relation is interpreted as a set oftuples (as in the Z language [43]). We assume that, for any
automaton A ¼ ðS; init; F ; ; C; Inv; T Þ, the domain of Inv
and T is always restricted to S. Note that not all of thepatterns are essential as some of them can be generated bycomposing other patterns. We will thus introduce thefundamental ones and then a set of derived ones.
Definition
3(EventPrefixing).
Let A ¼
ðS; init; F ; ; C; Inv; T Þ be a Timed Automaton. Let a be an
event. The event-prefixing pattern, i.e., the Timed Automaton
in which e precedes any action of A, written as
eventprefixða; AÞ, isðS [ finit0 g; init0 ; F ;  [ fag; C; Inv [ fðinit0 ; trueÞg;T [ fðinit0 ; a; ;; true; initÞgÞ;where init0 is a fresh state.

Event prefixing is considered one of the most commonlyused basic patterns, e.g., a task is preceded by some event.
In the above pattern, event a (which may be a synchronization barrier or variable assignment) must be engaged before
a certain task (which is modeled as A) must be carried out.
The fresh state init0 is connected to the initial state in A by atransition labeled with a.

3

TIMED AUTOMATA PATTERNSHigh-level real-time system requirements are often statedusing terms like deadline, time-out, and wait until, which can be
regarded as common timing constraint patterns. TCOZ,
designed to capture high-level system requirements, has arich set of hierarchical constructs that capture those common
timing patterns. In contrast, Timed Automata users often
need to manually cast those timing patterns into a set of clock
variables with carefully calculated clock constraints. In thissection, a rich set of composable Timed Automata patterns
is defined formally in order to facilitate high-level systemdesign using Timed Automata. Established compositional
patterns introduced in the classic CCS, CSP, Timed CSP,
and TCOZ are presented. The usefulness of the compositions is evidenced by early case studies on using thoseformalisms for system specification and analysis [31], [16],[13], [34]. Because we aim for efficient verification andcompositional modeling, the patterns are designed to be
simple, intuitive, and congruent to timed process algebra
operators.

3.1 Patterns
In the following, the Timed Automata patterns are
introduced one by one. First, the formal definition ispresented, followed by an intuitive graphic presentation.
Graphically, an automaton is abstracted as a triangle. The
left vertex of the triangle or a circle attached to the left
vertex represents the initial states. The right edge represents
the final states. The parallel composition of two automata is

D ef i n it i o n
4( I n t er n a l
Ch o i c e) .
L e t Ai ¼
ðSi ; initi ; Fi ; i ; Ci ; Invi ; Ti Þ where i 2 f1; 2g be two Timed
Automata. The internal choice of A1 and A2 , written as
intchoiceðA1 ; A2 Þ, isðS1 [ S2 [ finit0 g; init0 ; F1 [ F2 ; 1 [ 2 ; C1 [ C2 ;Inv1 [ Inv2 [ fðinit0 ; urgentÞg; T 0 Þ;
w h e r e init0 i s a f r e s h s t a t e a n d T 0 ¼ T1 [ T2 [fðinit0 ; ; ;; true; init1 Þ; ðinit0 ; ; ;; true; init2 Þg.

The above pattern captures nondeterminism, i.e., thesystem described nondeterministically behaves as either
A1 or A2 . Nondeterminism allows us to abstract away
irrelevant details of the system [27]. By introducing a fresh
state init0 and connecting init0 to initial states of bothautomata by unguarded transitions labeled with , thechoice is made internally and, thus, nondeterministically.
Because internal choice is symmetric and associative, wewrite intchoiceðA1 ; A2 ; . . . ; An Þ to denote the nondeterministic choice among multiple timed automata. Note that
init0 is urgent and, thus, no time elapsing is allowed. The
rule is that only additional states are marked urgent.
Marking states urgent allows us to systematically simplify
composed timed patterns (see example in Section 3.2).
Definition 5 (Recursion). Let A ¼ ðS; init; F ; ; C; Inv; T Þ bea Timed Automaton. Let S0 be a set of states such that S0  S.

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

DONG ET AL.: TIMED AUTOMATA PATTERNSThe recursion pattern, i.e., the Timed Automaton containing
recursive invocation of A at a state in S0 , written asrecurðA; S0 Þ, is ðS n S0 ; init; F n S0 ; ; C; Inv; T 0 Þ, whereT 0 ¼ T [ fðs; a; ; ; initÞj9s0 : S0  ðs; a; ; ; s0 Þ 2 T g.

Recursion is used to introduce infinite behaviors, which iscommonly used for specifying nonterminating reactive
systems. Given a timed automaton A and a set of states
S0 where there is a recursive call, the pattern is constructedby diverting all of the transitions to a state in S0 to the initialstate. Note that we request that S0 must be a proper subset
of S so as to prevent divergence. The dotted arrow
represents a transition that originally leads to a state in
S0 . In the resulting automaton, such transitions are
redirected to the initial state of A. This construction only
handles tail recursion. Note that we write recurðAÞ todenote recurðA; A:F Þ, i.e., the second argument is defaulted
to be the final states of A.
Definition 6 (Delay). Let t be a positive real number. The Timed
Automaton that delays the execution by t time units, written
as delayðtÞ, is ðfs1 ; s2 ; s3 g; s1 ; fs3 g; ;; fxg; Inv; T Þ, where
Inv ¼ fðs1 ; urgentÞ; ðs2 ; x  tÞ; ðs3 ; urgentÞg a n d T ¼
fðs1 ; ; fxg; true; s2 Þ; ðs2 ; ; ;; x ¼ t; s3 Þg.

The above pattern is used to delay the execution (of thesystem) by exactly t time units, e.g., one of the common
requirements for timed systems. We remark that internal
choice u, event prefixing a ! P , recursion, and WAIT may
be regarded as the fundamental blocking of Timed CSP
processes. This is justified by combining previous results onderiving a normal form for CSP/Timed CSP processes. In[9], it is proven that all CSP processes can be transformed
into a normal form, which composes only internal choices,
event prefixing, and process referencing.3 In [12], it isproven that the only fundamental building block of Timed
CSP processes (besides those of CSP) is WAIT. We may thus
prove that patterns that correspond to Timed CSP operators
can be generated from the fundamental ones (by transforming them into the normal form) by combining the above
results and proving a congruence theorem. In addition topatterns corresponding to Timed CSP constructs, two
additional patterns are introduced, namely, waituntil anddeadline. The wait-until pattern can be generated bycomposing other patterns (as we shall show later), whereas
the deadline pattern cannot. Thus, we regard the following
deadline pattern as fundamental too. Nonetheless, we givethe definitions of patterns corresponding to all TCOZ
operators for user convenience as well as efficiency reasons,i.e., a commonly used pattern may be manually optimized.
Definition 7 (deadline). Let A ¼ ðS; init; F ; ; C; Inv; T Þ be aTimed Automaton. Let t be a positive real number. The
deadline pattern deadlineðA; tÞ is
3. Or a chaotic process ? , which is irrelevant.

849

ðS [ finit0 g; init0 ; F ; ; C [ fxg; fðinit0 ; urgentÞg
[ fðs; invÞjs 2 S ^ inv ¼ ðInvðsÞ ^ x  tÞg;T [ fðinit0 ; ; fxg; true; initÞgÞ;where init0 is a fresh state and x is a fresh clock.

The above pattern is used to capture the requirement thatsome task must be finished by a certain time. It is more of arequirement than a design. Given a Timed Automaton A, if
it is constrained to finish within t time units, all states in A
are labeled with an invariant x  t in which x is a freshclock, which is reset when the control enters the automaton.
The leftmost state is the fresh state init0 . The local invariantx  t covers each state of the timed automaton and, thus, A
must terminate no later than t time units. This pattern may
introduce timelocks [6]. In particular, there might betime-actionlocks (i.e., situations in which neither time nor
action transitions can be performed) or zeno-timelocks (i.e.,situations in which time is unable to pass beyond a certain
point, but actions continue to be performed). Detecting andresolving timelocks is a highly nontrivial task (refer to [6]for sufficient conditions and sufficient and necessary
conditions for timelock-freeness). Nonetheless, we choose
to introduce this pattern simply because deadline is acommon real-time requirement. We may verify (e.g., using
the tool presented in [7] or UPPAAL) that A terminates
within t time units in all circumstances (so as to prevent
timelocks). Alternative ways of capturing deadlines arepresented in [3], [26].
Definition 8 (wait until). Let A ¼ ðS; init; F ; ; C; Inv; T Þ bea Timed Automaton. Let t be a positive real number. The waituntil pattern, written as waituntilðA; tÞ, isðS [ finit0 ; f 0 ; f 00 g; init0 ; ff 0 g; ; C [ fxg;
Inv [ fðinit0 ; urgentÞ; ðf 0 ; trueÞ; ðf 00 ; x  tÞg; T 0 Þ;
where init0 , f 0 , and f 00 are fresh states, x is a fresh clock, andT 0 ¼ T [ fðinit0 ; ; fxg; true; initÞg
[ fðf; ; ;; x t; f 0 Þjf 2 F g [ fðf; ; ;; x < t; f 00 Þjf 2 F g[ fðf 00 ; ; ;; x ¼ t; f 0 Þg:

The above pattern is used to constrain that a certain task
must take certain time units to finish. The automaton isconstrained to finish its process no earlier than t time units.
Given the automaton A, if the process of A finishes earlier
than t time units, then the system idles at a fresh state f 00
until exactly t time units elapses. Else if the process of A
takes more than (or exactly) t time units, the systemproceeds to final state f 0 without further waiting. Note that
this pattern can be generated from the delay pattern and theparallel composition pattern, i.e., it is straightforward toprove that waituntilðA; tÞ is equivalent to paraðA; delayðtÞÞ.

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

850

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,

Definition
9(External
Choice).
Let Ai ¼
ðSi ; initi ; Fi ; i ; Ci ; Invi ; Ti Þ where i 2 f1; 2g be two Timed
Automata. An external choice of A1 and A2 , written as
extchoiceðA1 ; A2 Þ, is paraðA01 ; A02 Þ, where
A01 ¼ ðS1 ; init1 ; F1 ; 1 ; C1 ; Inv1 ; fðs; ; ;  ^ x  0; s0 Þj
ðs; ; ; ; s0 Þ 2 T1 g [ fðs; x :¼ 1; ;  ^ x  0; s0 Þj
ðs; a; ; ; s0 Þ 2 T1 gÞ

VOL. 34,

NO. 6,NOVEMBER/DECEMBER 2008

ðS1 [ S2 [ finit0 g; init0 ; F1 [ F2 ; 1 [ 2 ; C1 [ C2 [ fxg;
Inv0 ; T 0 Þ;
where init0 is a fresh state, x is a fresh clock,
Inv0 ¼ fðinit0 ; urgentÞg [ fðinit1 ; Inv1 ðinit1 Þ ^ x  tÞg[ fðs; Inv1 ðsÞÞjs 2 S1 n finit1 gg [ fðs; Inv2 ðsÞÞjs 2 S2 g
and
T 0 ¼ T1 [ T2 [ fðinit0 ; ; fxg; true; initÞg
[ fðinit1 ; ;; x ¼ t; init2 Þg:

andA02 ¼ ðS2 ; init2 ; F2 ; 2 ; C2 ; Inv2 ; fðs; ; ;  ^ x 0; s0 Þj
ðs; ; ; ; s0 Þ 2 T2 g [ fðs; x :¼ 1; ;  ^ x 0; s0 Þj
ðs; a; ; ; s0 Þ 2 T2 gÞ;
where x : f1; 0; 1g is a fresh control variable.

The above pattern is useful when the choice is resolved by
the first action of either A1 or A2 . In the composition, thesystem may initially take a transition enabled in either A1 or
A2 . An initial state in the composition is a pair of initialstates ðinit1 ; init2 Þ, which is labeled transitions from either
init1 or init2 . Given automata A1 ; . . . ; An , the indexed
external choice is written as extchoiceðA1 ; . . . ; An Þ asextchoice is symmetric and associative. As external choice
is an operator of CSP, by applying the result in [9], it can be
resolved to a normal form containing only the fundamentalbuilding blocks.
Definition 10 (Sequential Composition). Let Ai ¼
ðSi ; initi ; Fi ; i ; Ci ; Invi ; Ti Þ where i 2 f1; 2g be two Timed
Automata. The sequential composition of A1 and A2 , written
as seqðA1 ; A2 Þ, isðS1 [ S2 ; init1 ; F2 ; 1 [ 2 ; C1 [ C2 ; Inv1 [ Inv2
[ fðs; urgentÞjs 2 F1 g; T Þ;
where T ¼ T1 [ T2 [ fðf; ; ;; true; init2 Þjf 2 F1 g.

Time out is a common behavior pattern in real-timesystems, which is partially evidenced by different ways
proposed to model it [21], [5], [40]. The fresh clock x is reset
along the transition from the fresh initial state to an initial in
A1 . Each initial state in A1 is constrained to make a move nolater than t time units. If the control moves out the initialstate before t time units, the system behaves as prescribedby A1 . Otherwise, after exactly t time units, A2 takes overthe control. If A1 may make a move at exactly time t, thesystem nondeterministically takes one of the transitions andprevents the other from happening. The timed-out pattern
can be generated using the external choice pattern and thedelay pattern.
Definition
12(TimedInterrupt).
Let Ai ¼
ðSi ; initi ; Fi ; i ; Ci ; Invi ; Ti Þ where i 2 f1; 2g be two Timed
Automata. Let t be a positive real number. The timed-interrupt
pattern, i.e., the Timed Automaton in which A1 is interrupted
by A2 after A1 starts execution for t time units, written as
timeinterðA1 ; A2 ; tÞ, i s ðS1 [ S2 [ finit0 g; init0 ; F2 ; 1 [
2 ; C1 [ C2 [ fxg; Inv0 ; T 0 Þ, where init0 is a fresh state, x
is a fresh clock,
Inv0 ¼ fðinit0 ; urgentÞg [ fðs; Inv1 ðsÞ ^ x  tÞjs 2 S1 g
[ Inv2 ;andGiven two Timed Automata A1 and A2 , the above shows thesequential composition. Sequential composition is commonly used to accomplish two tasks/jobs in order. By
linking the final states of A1 (i.e., the right edge) with theinitial state of A2 (i.e., the left vertex), the resulting
automaton passes control from A1 to A2 immediately after
A1 terminates. The transition from a final state in A1 to an
initial state in A2 is unguarded and labeled with . If A1 is
nonterminating, the final states in A2 may not be reachable.
Definition
11
(Time
Out).
L e t Ai ¼
ðSi ; initi ; Fi ; i ; Ci ; Invi ; Ti Þ where i 2 f1; 2g be two Timed
Automata. Let t be a positive real number. The time-out
pattern, written as timeoutðA1 ; A2 ; tÞ, is

T 0 ¼ T1 [ T2 [ fðinit0 ; ; fxg; true; init1 Þg[ fðs1 ; ; ;; x ¼ t; init2 Þjs1 2 S1 g:

The pattern is composed of two automata, A1 and A2 . The
fresh state init0 and clock x are used similarly as in theprevious patterns. Every state in A1 is constrained to make amove before t time units. After t time units elapse, thecontrol transfers from one of the state in A1 (not necessarily
a final state) to the initial state in A2 . Note that theinterruption is preemptive, i.e., transitions in A1 areprevented from happening once t time units have elapsed.

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

DONG ET AL.: TIMED AUTOMATA PATTERNS

851

Fig. 2. Composing timed patterns.

Definition
13(eventinterrupt).
Let Ai ¼
ðSi ; initi ; Fi ; i ; Ci ; Invi ; Ti Þ where i 2 f1; 2g be two Timed
Automata. Let a be an event. The event-interrupt pattern, i.e.,
the Timed Automaton in which A1 is interrupted whenever
event a engages and then the control transfers to A2 , written
as evtinterðA1 ; A2 ; aÞ, isðS1 [ S2 ; init1 ; F1 [ F2 ; 1 [ 2 [ fag; C1 [ C2 ;Inv1 [ Inv2 ; T 0 Þ;
where T 0 ¼ T1 [ T2 [ fðs1 ; a; fxg; true; init2 Þjs1 2 S1 g.

Example. Assume that the requirement is that “a task must
be repeated every t time units (the hidden requirement isthat the task must terminate before t time units).” A newpattern, named periodic-repeat can be generated bycomposing the deadline, wait-until, and recursion patterns.
Let A ¼ ðS; init; F ; ; C; Inv; T Þ be the automaton modeling the task. By Definition 7, deadlineðA; tÞ isðS [ fi1 g; i1 ; F ; ; C [ fxg; fði1 ; urgentÞg
[ fðs; InvðsÞ ^ x  tÞjs 2 Sg; T [ fði1 ; ; fxg; true; initÞgÞ:By Definition 8,
waituntilðdeadlineðA; tÞÞ ¼ ðS1 ; init1 ; F1 ; C1 ; Inv1 ; T1 Þ;
whereEvent interrupt is similar to timed interrupt except that,
because there are no timing constraints involved, no
additional state or clock is necessary. Instead, an unguarded
transition labeled with a is created from each state in A1 toan initial state in A2 .
Definition 14 (Timed-Event Prefixing). Let A ¼
ðS; init; F ; ; C; Inv; T Þ be a Timed Automaton. Let a be an
event. Let t be a positive real number. The timed-eventprefixing pattern, i.e., the Timed Automaton in which a
engages at time t and precedes any action of A, written as
teventprefixða; t; AÞ, is
0

00

0

ðS [ finit ; init g; init ; F ;  [ fag; C [ fxg;
Inv [ fðinit0 ; urgentÞ; ðinit00 ; trueÞg; T 0 Þ;
w h e r e init0 ; init00 a r e f r e s h s t a t e s a n d T 0 ¼ T [fðinit0 ; ; fxg; true; init00 Þ; ðinit00 ; a; t :¼ x; ;; true; initÞgÞ.

S1 ¼ S [ fi1 ; i2 ; f1 ; f2 g; init1 ¼ i2 ; F1 ¼ ff1 g;
1 ¼ ; C1 ¼ C [ fx; yg;
Inv1 ¼ fðs; InvðsÞ ^ x  tÞjs 2 S g [ fði1 ; urgentÞ; ði2 ; urgentÞ;ðf1 ; trueÞ; ðf2 ; x  tÞg;T1 ¼ T [ fði1 ; ; fxg; true; initÞg [ fði2 ; ; fyg; true; i1 Þg[ fðf; ; ;; y t; f1 Þjf 2 F g [ fðf; ; ;; y < t; f2 Þjf 2 F g[ fðf2 ; ; ;; y ¼ t; f1 Þg:
The periodic-repeat pattern isperiodicrepeatðA; tÞ ¼ recurðwaituntilðdeadlineðA; tÞÞÞ;which is denoted as ðS1 ; init2 ; F2 ; 2 ; C2 ; Inv2 ; T2 Þ. By
Definition 5, we have
S2 ¼ S [ fi1 ; i2 ; f2 g; init2 ¼ i2 ; F2 ¼ ;; 2 ¼ ;
C2 ¼ C [ fx; yg;
Inv2 ¼ fðs; InvðsÞ ^ x  tÞjs 2 S g [ fði1 ; urgentÞ;ði2 ; urgentÞ; ðf2 ; x  tÞg;T2 ¼ T [ fði1 ; ; fxg; true; initg [ fði2 ; ; fyg; true; i1 Þg[ fðf; ; ;; y t; i2 Þjf 2 F g [ fðf; ; ;; y < t; f2 Þjf 2 F g

Because t is the time taken from the moment this pattern isenabled to the time event a is engaged, a fresh clock x is
initiated whenever the automaton is enabled. The readingof x at the time when a is engaged is recorded in t.

3.2 Composing Patterns
Our experience [16], [13], [37] shows that the patterns
presented above cover most of the common timed patterns.
Nonetheless, the patterns are by no means complete. New
useful patterns can be added into our library or composedfrom the existing ones. In the following, we show how to build
new patterns by composing multiple existing patterns.

[ fðf2 ; ; ;; y ¼ t; i2 Þg:Note that, because the only final state f1 is replaced by arecursive call at the last step, the automaton isnonterminating (as expected) and, hence, has no final
states. The transformation is visualized in Fig. 2. The
resulting automaton is the one on the left. Because
state i1 (the second state from left) is urgent, at any
moment x ¼ y, the automaton is simplified to be the rightone ( transitions have been removed). The two diverted
transitions are merged into one because they are only
enabled when the reading of clock x or y is t.

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

852

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,

It is important that the Timed Automata patterns
combine with the bottom-up composibility (of process
algebra style) because complex real-time systems may benaturally modeled as collections of subcomponents at
different abstraction levels. In the bottom-up design
process, a subcomponent of reasonable complexity (andwhich is flattened) may be modeled as a Timed Automaton.
The system can then be naturally composed from themodeling of the subcomponents. The Timed Automata
patterns provide user-friendly templates to build such
hierarchical modeling. In the top-down design process,the modeling of a complex system can be generated byrefining the components, step by step, using appropriate
patterns until it is simple enough to be modeled as aflattened Timed Automaton. As a reasonable price to pay, asystem design based on Timed Automata patterns may
require extra states or clocks, for instance, Definitions 7, 8,
and 14 introduce new states and clocks. However, ourexperience shows that the extra states and clocks often canbe removed using simple optimization procedures, e.g.,-transition reduction (if the outgoing transitions of a state
are all -transitions, remove the state and redirect all
incoming transitions), urgent states reduction, or reusing
clocks that are no longer referenced (which is common as
clocks are local to one Timed Automaton).

4

TRANSLATING TIMED PROCESS ALGEBRA TO
TIMED AUTOMATA

A practical implication of the Timed Automata patterns isthat process-algebra-based specification languages like
Timed CSP or TCOZ can be systematically translated to
Timed Automata so as to benefit from the verification
mechanism of Timed Automata. In this section, a translation from TCOZ to Timed Automata is defined (which
implies a translation from Timed CSP to Timed Automata).
The following defines the Timed Automaton interpretationof the primitive processes.
Definition 15 (primitives). Let Op be a data operation (or an
operation schema):
Askip ¼ ðfi; fg; i; ffg; fg; ;; fði; urgentÞ; ðf; trueÞg;fði; ; ;; true; fÞgÞ;Astop ¼ ðfig; i; ;; ;; ;; fði; trueÞg; ;Þ;
AOp ¼ fi; fg; i; ffg; feOp g; ;; fði; trueÞ; ðf; trueÞg;ði; eOp ; ;; pre Op; fÞ ;where eOp is an atomic event representing the data operationand pre Op is its precondition [43].
Askip allows an unguarded transition from its initial state to
the final state. Because the initial state is urgent, theautomaton terminates immediately. Astop allows no transitions at all (and so, no final state is reachable). A data
operation is presented as a Timed Automaton with only one
transition. The transition is guarded with the precondition

VOL. 34,

NO. 6,NOVEMBER/DECEMBER 2008of the operation and labeled with an event that represents
the atomic data change. The control may reside at the initialstate for some time as the data operation may not be
instantaneous.
Definition 16 (translation). Let P be the set of all TCOZ
processes. Let A be the set of all Timed Automata. A
translation is a function M : P ! A defined as follows:MðSKIPÞ
MðSTOPÞMðOpÞ
Mða ! P Þ
Mða@t ! P ÞMðWAIT tÞMðP  WAITUNTIL tÞMðP  DEADLINE tÞ
M ðP . ftgQÞ
M ðP 4 ftgQÞ
MðP 4 a ! QÞMðP ; QÞMðP tuQÞMðP u QÞMðP kQÞ
M ðX  P ðXÞÞ

¼ Askip¼ Astop ;¼ AOp ;
¼ eventprefixða; MðP ÞÞ;¼ teventprefixða; t; MðP ÞÞ;¼ delayðtÞ;¼ waituntilðMðP Þ; tÞ;¼ deadlineðMðP Þ; tÞ;¼ timeoutðMðP Þ; MðQÞ; tÞ;¼ timeinterðMðP Þ; MðQÞ; tÞ;¼ evtinterðMðP Þ; MðQÞ; aÞ;¼ seqðMðP Þ; MðQÞÞ;¼ extchoiceðMðP Þ; MðQÞÞ;¼ intchoiceðMðP Þ; MðQÞÞ;¼ paraðMðP Þ; MðQÞÞ;¼ recurðM ðP ðXÞÞ; SX Þ;

where P and Q are processes, a is an event, t is a positive real
number, and SX is a set of states where X is invoked.
Note that recursion in the above definition relies on SX . A
recursive process is translated like a normal process except
that, whenever there is a recursive call X, instead of unfolding
X as a Timed Automaton, a state is created and the state isadded to SX . The rest of the translation is mostly selfexplanatory. For instance, P  DEADLINE t constrains that P
must terminate no later than t. This process is translated todeadlineðMðP Þ; tÞ in which MðP Þ is the Timed Automaton
capturing the behaviors of process P . The resulting automaton differs from MðP Þ in that it must terminate before
t time units, which is the semantics of the TCOZ expression
P  DEADLINE t. Other mapping rules can be explained
similarly. By applying M iteratively, a process is translated
to a flattened Timed Automaton straightforwardly.
Example. We use the timed queue example to illustrate thetranslation and hint how the timed patterns can beapplied to facilitate system design using Timed Automata. If TCOZ is used to specify the queue in the firstplace, by applying M to the MAIN process, a Timed
Automaton specification of the queue can be generated
step by step. Because the generated Timed Automata are
behaviorally equivalent to the TCOZ processes (shown
below), the analysis results on the generated Timed
Automata apply to the original TCOZ specification:

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

DONG ET AL.: TIMED AUTOMATA PATTERNS

853

Fig. 3. Timed Automaton of a timed queue where e1, e2, and e3 are eJoin , eLeave , and eDel , respectively.

MðMAINÞ¼ M ðQ  ðJoin t
u LeaveÞ . fTo gðDel  DEADLINE Tl Þ; QÞ¼ recurðMðJoin t
u LeaveÞ . fTo gðDel  DEADLINE Tl Þ; QÞ; SQ¼ recurðseqðMðJoin t
u LeaveÞ . fTo gðDel  DEADLINE Tl ÞÞ; MðQÞ; SQ¼ recurðseqðtimeoutðMðJoin t
u LeaveÞ;MðDel  DEADLINE Tl Þ; To Þ; MðQÞÞ; SQ¼ recurðseqðtimeoutðextchoiceðMðJoinÞ;MðLeaveÞÞ; deadlineðMðDelÞ; Tl Þ; To Þ; MðQÞÞ; SQ¼ recurðseqðtimeoutðextchoiceðAJoin ; ALeave Þ;deadlineðADel ; Tl Þ; To Þ; MðQÞÞ; SQ :As discussed above, a recursive call shall not be
unfolded. For instance, MðQÞ in the above is viewed aTimed Automaton with only one state (which is both theinitial and final state), which later will be removed
because of the recursion pattern. By applying thedefinitions in Section 3.1 in a bottom-up manner,MðMAINÞ is flattened to the one in Fig. 3b. Note thatstate Q corresponds to the recursive call of process Q.
The Timed Automaton can be further reduced to Fig. 3aby removing -transitions (e.g., the transitions from f2,
f1, and f3 to f6) and the urgent state f5 and reusing
clocks (e.g., instead of x, reuse y).
Alternatively, Timed Automata users can do a topdown design using the patterns in the same modular
way that TCOZ users do hierarchical system design, thatis, to assume the availability of lower level processes orTimed Automata that behave in a certain way, specify
the system in terms of the lower level processes or Timed
Automata (e.g., at the top level, a designer may
intuitively decide that the queue must be recursive andtherefore apply the recursion pattern), and then iteratively refine each lower level process or Timed Automaton until they are simple enough to be modeled as asimple process or a flattened Timed Automaton.
In the following, we prove that the translation M issound, i.e., given any process P , the automaton MðP Þ isbehaviorally equivalent to P . We show that there is a weakbisimulation relation (which implies behavioral equivalence) between the transition system semantics of a process
and the automaton. This also justifies that the patterns
capture intuitive meanings.
Definition 17 (TCOZ Semantics). Let P be the set of all TCOZ
processes. Let P be a process. Let T
T be the time domain.
T; ðP ; tÞ;  [ TT; !1 Þ is a labeled transition
T SP1 ¼ ðP  T
system where P  T
T is the state space, ðP ; tÞ : P  T
T is aninitial state,  is a set of events, and !1 is a labeledtransition relation that is defined by the rules in Appendix A,
which can be found on the Computer Society Digital Library at
http://doi.ieeecomputersociety.org/10.1109/TSE.2008.52,
awhere c !1 c0 ðc; a; c0 Þ 2 !1 .
Most of the rules (i.e., the operational semantics) can bereferenced in Schneider’s book [40], except those rules thatare TCOZ-specific, e.g., DEADLINE and WAITUNTIL. In thenext definition, -transitions in T SP1 are abstracted away
because only observable behaviors are concerned.4
Definition 18 (Observable TCOZ Semantics). Let P be theset of all TCOZ processes. Let P be a process. Let T
T be the timeT; ðP ; tÞ;  [ TT; ¼)1 Þ is a labeled
domain. T SP2 ¼ ðP  Ttransition system where P  T
T is the state space, ðP ; tÞ :PT
T is an initial state,  is the set of possible events
including the internal event , and ¼)1 is a labeled transitionT,
relation such that for any c; c0 : P  T
.

a



a











b 9c1 ; c2  c !1 c1 !1 c2 !1 c0 , andc ¼)1 c0 ¼

b 9c1 ; c2  c !1 c1 !1 c2 !1 c0 ,. c ¼)1 c0 ¼
where the relation !1 is the sequential composition of a
finite number of !1 .
T SP2 differs from T SP1 in that all -transitions are hidden.
Next, we define the semantics of Timed Automata. A
transition system semantics of Timed Automata has been
defined in [2], [10].
Definition 19 (Timed Automata semantics). Let A ¼
ðS; init; F ; ; C; Inv; T Þ be a Timed Automaton. Let V be
the valuations of clocks. T SA1 ¼ ðS  V ; ðinit; v0 Þ;  [b  V is the state space. The initial state s0 ¼
T
T; !2 Þ: ¼Sðinit; v0 Þ comprises the initial state init and a zero valuationTÞ  S is a transition relation comprisv0 . !2  S  ð [ T
ing either time passing ðs; vÞ !2 ðs; v þ Þ or, if thetransition ðs; a; ; ; s0 Þ is enabled, an action executionðs; vÞ !2 ðs0 ; v0 Þ.
Similarly, we define the transition system where all
-transitions are hidden.
Definition 20 (Observable Timed Automata Semantics).
Let A ¼ ðS; init; F ; ; C; Inv; T Þ be a Timed Automaton.
Let V be the valuation of the clocks. T SA2 ¼ ðS T; ¼)2 Þ: S  V is the state space. The
V ; ðinit; v0 Þ;  [ Tinitial state s0 ¼ ðinit; v0 Þ comprises the initial state init and4. We assume that the processes are divergence free, i.e., only finite
numbers of consecutive  transitions are possible.

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

854

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,

a zero valuation v0 . ¼)2  S  ð [ TTÞ  S is a labeledtransition relation such that, for all s; s0 : S  V ,
a



a











.

b 9s1 ; s2  s !2 s1 ¼)2 s2 !2 s0 , ands ¼)2 s0 ¼.

b 9s1 ; s2  s !2 s1 ¼)2 s2 !2 s0 ,s ¼)2 s0 ¼
where the transition relation !2 is the sequential composition of at most a finite number of !2 .
With the above preparation, a bisimilar (homomorphic)
relation between T SP2 and T SA2 is readily defined.
Definition 21 (Bisimulation). Let T Si ¼ ðSi ; initi ; i ; Ti Þ
where i 2 f1; 2g be two labeled transition systems. For any
s1 2 S1 and s2 2 S2 , s1 s2 if and only if
8ðs1 ; a; s01 Þ : T1  9s02 2 S2  ðs2 ; a; s02 Þ 2 T2 ^ s01 s02
and. 8ðs2 ; a; s02 Þ : T2  9s01 : S1  ðs1 ; a; s01 Þ 2 T1 ^ s01 s02 .
T S1 and T S2 are bisimilar, written as T S1 T S2 , if and only
if init1 init2 .
.

The following theorem states that the translation in
Definition 16 is sound, i.e., the source and target transition
systems are bisimilar. The proof is presented inAppendix B, which can be found on the Computer Society
Digital Library at http://doi.ieeecomputersociety.org/
10.1109/TSE.2008.52.
Theorem 1 (soundness). Let P be a TCOZ process. Let T SP2 ¼
ðP  T
T; ðP ; tÞ;  [ TT; ¼)1 Þ as defined above. Let A ¼
MðP Þ ¼ ðS; init; F ; ; C; Inv; T Þ: L e t
T SA2 ¼ ðS 2T; ¼)2 Þ as defined above. T SP T SA2 .
V ; ðinit; v0 Þ;  [ T

4.1 Implementation
In order to assist system development using either TCOZ or
Timed Automata, we have developed a prototype supporting functionalities including automated translation fromTCOZ specification to Timed Automata (for TCOZ users tobenefit from the supporting tools of Timed Automata) andhigh-level system design using Timed Automata (refer tothe next section).
The translation from TCOZ to Timed Automata is
automated by employing XML and Java technology. In
our previous work, the syntax of the Z family languages(i.e., Z/OZ/TCOZ) has been defined using XML schemas,
which is named ZML [42]. A number of tools based on XML
representation of TCOZ models have been developed.
UPPAAL also supports an XML representation of Timed
Automata. Hence, the translation is reduced to a conversion
from one XML file to another. Our tool reads a TCOZ
specification represented in XML and outputs an XML
representation of a Timed Automaton specification conforming to the DTD syntax defined in UPPAAL. The
translation rules are used as a design document to transform the process aspects of a TCOZ specification. Worthy ofmention is that, because TCOZ allows synchronization
among multiple parties, whereas UPPAAL allows only
pairwise synchronization, committed states are used toachieve broadcasting communication in the target UPPAAL
model (detailed information can be found in [33]). In
addition, the following handles the data aspects. A channel
communication may carry a value in TCOZ, which is not

VOL. 34,

NO. 6,NOVEMBER/DECEMBER 2008

possible in UPPAAL. Value passing in UPPAAL is achieved
by global variable assignments along the Timed Automatatransitions. A class in TCOZ is translated to a Timed
Automaton template in UPPAAL (by translating the MAIN
process of the class). Instances of the class are translated as
instances of the template. The predicate in the INIT schemaof a TCOZ class is labeled with the initial state of theresultant Timed Automaton. UPPAAL supports limited
data types, e.g., bounded integers, arrays of bounded
integers, record types, scalars, etc. Thus, only those datatypes are allowed for the translation at the current stage.

5

CASE STUDY: RAILCAR SYSTEM

The system design based on TCOZ is to identify objects andtheir data attributes from the system requirements, encapsulate relevant data operations, as well as dynamic
behavior patterns, in the respective object modeling, and,
finally, compose different objects to form the system
specification. Because of the bottom-up composibility ofprocess algebra (which TCOZ is based on), modeling the
dynamic behaviors in TCOZ is compositional and natural.
The system design based on Timed Automata patterns
enjoys similar composibility, i.e., starting with building
Timed Automata designs of fractions of the system andthen composing the basic Timed Automata using the timed
patterns. In this section, a Railcar System is used todemonstrate a high-level real-time system design using
both Timed Automata patterns and TCOZ. This system was
inspired by the railcar system presented in [24].

5.1High-Level System Design Using Timed
Automata
In the Railcar System, there are four (possibly more)terminals that are located in a cyclic path. Each terminal
contains a push button for passengers to place theirrequests for car service. A railcar travels clockwise on the
track to transport passengers between terminals. The railcar
is equipped with a destination board to receive internal
requests and to indicate each destination terminal. There isa central control that receives, processes, and sends data to
the terminals and the railcar so that external requests fromany terminal can be fulfilled. Additional timing requirements are added into the original model [24] because
quantitative timing is an important aspect of the system, as
illustrated in the following scenarios:
Before the railcar leaves a terminal, it sends a signal
to depart to the terminal. The terminal prepares forthe railcar to depart and responds to the railcar
within 5 seconds. The railcar then leaves theterminal and cruises toward the destination.
. When the railcar comes to a stop at a terminal, it
opens its door for exactly 10 seconds. After that, it
closes the door and begins to wait for either internal
passenger requests or an external request dispatchedfrom the controller. Passengers inside the railcar are
given 5 seconds to make an internal request before
the railcar accepts any external requests.
Designing the system from scratch using ordinary Timed
Automata is nontrivial. The system is composed of multiple
objects, each of which are assigned with different behavior
patterns, e.g., the controller is responsible for handling.

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

DONG ET AL.: TIMED AUTOMATA PATTERNS

Fig. 4. A structural design.

different tasks. Nonetheless, the requirements of the system
are naturally captured in a hierarchical way [24]. Using thetimed patterns, we achieve a similar approach to model thesystem as in [24]. The Railcar System has three components,
i.e., a railcar, the terminals, and a central controller. The
railcar is composed of three basic components, i.e., a car
destination panel, a car door, and a car handler. There is abutton at each terminal so that passengers can request for aservice. The central controller maintains a record of all
external requests and dispatches external requests to the855

railcar if there is any. All system components are connectedby channels. Fig. 4 shows a hierarchical blueprint of thesystem, where a triangle represents a Timed Automaton
and a double-arrowed dotted line means that there arecommunications in between. Each triangle will be detailed
in the following. For each component, we will first identify
the basic behaviors (of manageable complexity) and thencompose them to build the system step by step.
Let terminalðiÞ, where i 2 f1; 2; 3; 4g, be the four terminals. Let tb i : IB be a local variable to terminalðiÞ
representing the button at the ith terminal. tb i ¼ true if
and only if the button is lit. The four automata in Fig. 5ashow the basic behaviors of a terminal. In automaton
P ressButtonðiÞ, where i 2 f1; 2; 3; 4g, an external request
enters the external request queue in the central controller
only if the button has not been pressed before. Oncepressed, the light is on (i.e., tb i :¼ true). In ButtonOff, oncethe controller informs the terminal that the request has been
serviced, the light goes off. In T erApproach, event
approach req signals the approaching of the car, and theFig. 5. Basic behavior patterns.
Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

856

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,

VOL. 34,

NO. 6,NOVEMBER/DECEMBER 2008

Fig. 6. Composed behaviors (1).

Fig. 7. Composed behaviors (2).

terminal does the necessary preparation (abstracted as adelay in this modeling) and then acknowledges. Last, in
T erDepart, before the car departs, the terminal is informed
by depart req and acknowledges by depart ack. The
composed behavior of a terminal isterminalðiÞ ¼ recurðextchoiceðP ressButton; ButtonOff;
T erApproach; T erDepartÞÞ;where PressButton = extchoice(PressButton(1), PressButton(2), PressButton(3), PressButton(4)). The terminals are
specified as Terminals = para(terminal(1), terminal(2),terminal(3), terminal(4)).
We model the behaviors of the car similarly. The door
has been modeled in Section 2.1. The panel in the car iscomposed of four buttons. Let b be an array of Boolean
variables. b½i ¼ true, where i 2 f1; 2; 3; 4g, means theith button has been lit already. Let curr and dest be two
global variables that record the station the car is approaching and the destination, respectively. Let tostop : IB be a
global variable that says whether to stop or not at the next
terminal. The automata in Fig. 5b model the basic behaviorsof the panel. In automaton IntRequest, a passenger in the
car may press a button on the panel (modeled as event
int request i, where i 2 f1; 2; 3; 4g) and the button is lit
afterward. Note that the button may be pressed even if it
has been pressed already. In IntSchedule, if there is aninternal request, the car panel computes the next destination once an input is received on channel int sched (fromthe car handler). The destination is set to be the next
requested terminal. In IntCheck (when the car is approaching the next terminal), the car handler orders the panel tocheck whether there is an internal request for the next
terminal and decides whether to stop at the next terminal.
The overall behaviors of the panel are specified as P anel ¼
recurðextchoiceðIntRequest; IntSchedule; IntCheckÞÞ.
The behavior patterns of the central controller are similar
to those of the panel except that the car panel handles internal
requests, whereas the controller handles external requests.
The automata in Fig. 5c model its basic behaviors. Let eb be anarray of Boolean variables that represents whether theexternal buttons have been pressed and lit. The overallbehaviors of the controller are specified as Controller =recur(extchoice(ExtRequest, ExtSchedule, ExtCheck)).

The automata in Fig. 5d model the basic computational
logic of the car handler. In order to specify its overallbehaviors, we make use of the timed patterns. The
compositional Timed Automaton named Moving, presented
in Fig. 6, specifies the behaviors of the car handler aftergetting a request (either from internal or external). If thedestination is the current terminal, the car door is opened.
Otherwise, the car leaves the terminal and heads toward thedestination. Once approaching the next terminal, the carchecks if there is a newly arrived request from external orinternal for the approaching terminal. Afterward, theautomaton repeats from the beginning. Note that thishierarchical automaton has already been partially flattenedfor simplicity.
The overall behavior of the car handler can be composedfrom the above basic one. Initially, the car handler is idlingat some terminal. It waits for an internal request first. If aninternal request arrives within 4 seconds, it starts to serve
the request. Otherwise, it waits for either an internal orexternal request and then starts moving. Once it reaches thedestination, it repeats from the beginning. The overallbehavior of the car handler is represented as follows:
CarHandler ¼ recurðseqðtimeoutðIntSchedule; extchoiceðIntSchedule; ExtScheduleÞ; 4Þ; MovingÞÞ:Graphically, it is drawn as shown in Fig. 7. Last, the systemis the parallel composition of the three components, i.e.,para(Terminals, Controller, para(Panel,Door,CarHandler)).

5.2 Analysis of the TCOZ Modeling
Based on the strength of OZ and Timed CSP, TCOZ
supports object-oriented design of data structures, as wellas compositional design of dynamic behaviors, as demonstrated in [37], [36]. Because modeling using TCOZ (whichshares the same bottom-up nature as using the Timed
Automata patterns) is largely irrelevant to this paper, weshow instead how the TCOZ specification is translated to
Timed Automata systematically using our prototype andthen verified using UPPAAL. The relevant part of the TCOZ
specification is presented in Appendix C, which can befound on the Computer Society Digital Library at http://
doi.ieeecomputersociety.org/10.1109/TSE.2008.52.

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

DONG ET AL.: TIMED AUTOMATA PATTERNSEach active class in the TCOZ model is projected to a
Timed Automaton template, namely, a terminal template
for the class T erminal; a car door, a car destination panel,and a car handler template for the class CarDoor, CarP anel,
and CarHandler, respectively; and a controller template forthe class Controller. The terminal template has four
instances, which represents the four different terminals
according to the TCOZ specifications. The other templates
have only one instance. The translation is a straightforward
application of Definition 16. We use the T erminal class as
an example to show the identification of the states,transitions, guards, and synchronization. Its processes
mainly have an external choice pattern and a recursion
pattern as defined by its MAIN process:recurðextchoiceðMðP ressDownÞ; MðDownOffÞ;MðCarApproachÞ; MðCarDepartÞÞ; SP Þ:
By applying the translation to each of the processes
P ressDown, DownOff, CarApproach, and CarDepart, we
obtain the Timed Automaton template of the class
T erminal. The above translation is automated by ourtranslation tool. Then, by adding the object reference
information manually, such as the identification of eachdifferent terminal, the whole automaton can be visualizedin UPPAAL. Similarly, Timed Automata are generated fromother system components, e.g., the template for class Dooris shown in Section 2.1. The translation result is stored in an
XML format, which can be readily imported by UPPAAL.
Now, we can use the simulator and verifier of UPPAAL tosimulate the system, as well as to model check someinvariants and real-time properties. The key point of therailway system is to provide efficient services. The following are some of the properties that can be formally specified
and verified using UPPAAL:
Prop1. Whenever the car destination board receives arequest to a terminal, say, terminal 1, the railcar will
eventually get to that terminal within 600 seconds. It
can be translated into a Timed CTL as a bounded
liveness property.
. Prop2. The door must be open for no more than
10 seconds.
. Prop3. The system is deadlock free.
. Prop4. Whenever the railcar is moving, the car door
is closed.
UPPAAL verified that these properties hold for this given
model. As for reference, the time consumption for analyzing each of the properties is listed below. The experimentresults are obtained on the Windows XP platform with
2 Gbyte memory and Intel 3.0 GHz CPU. N is the number ofterminals.
.

857

In summary, the Timed Automata patterns allow us toenjoy a hierarchical system design using Timed Automata,i.e., to apply a divide-and-conquer strategy to deal with thecomplexity of the system design. A high-level design (as theone above where highly coupled system behaviors areencapsulated in one component) is easier to understand andmaintain. A high-level system design can be automaticallyflattened (by applying the definitions plus optimization
techniques for reducing the number of states, as well as
clocks) and then verified using existing tools like UPPAAL.
Compared to the system design using timed patterns
directly, which solely focuses on dynamic behaviors, the
TCOZ-based design is heavy in modeling data andfunctional aspects of the system. Because the timed patterns
are closely related to compositional operators in TCOZ, themodeling of dynamic behaviors using timed patterns and
TCOZ share similar ideas.

6

CONCLUSION

For the last decades, a variety of formal modeling/
specification languages have been proposed for real-timesystem design and verification. The various modeling andverification techniques all have similarities and differences
to some degree. It is important for the formal method
community to understand how various techniques differ
from each another and how they may benefit from eachother. The techniques under consideration, namely, TCOZ/
Timed CSP and Timed Automata, deal with behavioral realtime aspects of systems. Lying at each end of the spectrumof formal modeling techniques, TCOZ is designed for the
structural specification of high-level complex system
requirements, whereas Timed Automata are used to design
timed models with simple clock constraints but with highly
automated verification support. In this work, we studied
both formalisms from a practical point of view, i.e., how canthey help each other? We are not arguing which of the two
is superior. Instead, we enrich TCOZ with verification
support by translating its models to Timed Automata andenrich Timed Automata with composable patterns for highlevel system design.
The main contribution of the work is the rich set of timed
patterns, which covers all common hierarchical systembehaviors like deadline, timeout, and timedinterrupt. These
patterns are formally defined so as to achieve composibility inthe graphical representations. Moreover, we have shown thatnew timed patterns may be composed naturally using ourtimed patterns. These patterns not only provide a proficientinterchange media for translating time-enriched process
algebra specifications into Timed Automata but also provide
a generic reusable framework for developing real-timesystems solely using Timed Automata. As shown in Section 5,
by decomposing a complex system to subcomponents ofmanageable size and then composing the subcomponents
using timed patterns, these patterns offer a systematic way offighting the great complexity in system design.
One of the future works is to develop fully automatedoptimization techniques that could maximally reduce thenumber of states and clocks while flattening the Timed
Automata patterns. This is important because the numberof clocks (and states) has a significant impact on theperformance of tools like UPPAAL. Another future work
is to integrate our prototype with UPPAAL for user

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

858

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,

convenience. A future work of theoretical interest is to
fully compare the expressiveness of timed process
algebras like Timed CSP and Timed Automata so as togain better support for verifying real-time systems.

ACKNOWLEDGMENTS
The authors would like to thank Hugh Anderson, Roger
Duke, Sun Jing, Wang Hai, Lars Grunske, and theanonymous referees for their insightful comments on thiswork. This research is partially supported by the research
grant R-252-000-201-112 funded by National University ofSingapore. Jun Sun is the corresponding author for thispaper.

REFERENCES
[1]
[2]
[3]
[4]
[5]
[6]
[7]
[8]
[9]
[10]
[11]
[12]
[13]

[14]
[15]
[16]
[17]
[18]
[19]
[20]
[21]

R. Alur, C. Couroubetis, and D.L. Dill, “Model-Checking for RealTime Systems,” Proc. Fifth Ann. IEEE Symp. Logic in Computer
Science, pp. 414-425, 1990.
R. Alur and D.L. Dill, “A Theory of Timed Automata,” TheoreticalComputer Science, vol. 126, pp. 183-235, 1994.
S. Bornot and J. Sifakis, “Relating Time Progress and Deadlines inHybrid Systems,” Proc. Int’l Workshop Hybrid and Real-Time
Systems, pp. 286-300, 1997.
S. Bornot, J. Sifakis, and S. Tripakis, “Modeling Urgency in Timed
Systems,” Proc. Int’l Symp. Compositionality: The Significant
Difference, pp. 103-129, 1997.
H. Bowman, “Modelling Timeouts without Timelocks,” Proc. Fifth
Int’l AMAST Workshop Formal Methods for Real-Time and Probabilistic Systems, pp. 334-353, 1999.
H. Bowman and R. Gómez, “How to Stop Time Stopping,” Formal
Aspect of Computing, vol. 18, no. 4, pp. 459-493, 2006.
H. Bowman, R. Gómez, and L. Su, “A Tool for the Syntactic
Detection of Zeno-Timelocks in Timed Automata,” Electronic Notes
in Theoretical Computer Science, vol. 139, no. 1, pp. 25-47, 2005.
P. Brooke, “A Timed Semantics for a Hierarchical Design
Notation,” PhD dissertation, Univ. of York, 1999.
S.D. Brooke, “A Model for Communicating Sequential Processes,”
PhD dissertation, Oxford Univ., 1983.
A.M.K. Cheng, Real-Time Systems: Scheduling, Analysis, andVerification. John Wiley & Sons, 2002.
A. David and M.O. Möller, “From HUPPAAL to UPPAAL: A
Translation from Hierarchical Timed Automata to Flat Timed
Automata,” Technical Report RS-01-11, BRICS, Mar. 2001.
J. Davies, Specification and Proof in Real-Time CSP. Cambridge
Univ. Press, 1993.
J.S. Dong, N. Fulton, L. Zucconi, and J. Colton, “Formalizing
Process Scheduling Requirements for an Aircraft Operational
Flight Program,” Proc. First IEEE Int’l Conf. Formal Eng. Methods,
pp. 161-169, 1997.
J.S. Dong, P. Hao, S.C. Qin, J. Sun, and W. Yi, “Timed Patterns:
TCOZ to Timed Automata,” Proc. Sixth Int’l Conf. Formal Eng.
Methods, pp. 483-498, 2004.
J.S. Dong, P. Hao, J. Sun, and X. Zhang, “A Reasoning Method forTimed CSP Based on Constraint Solving,” Proc. Eighth Int’l Conf.
Formal Eng. Methods, pp. 342-359, 2006.
J.S. Dong, B.P. Mahony, and N. Fulton, “Modeling Aircraft
Mission Computer Task Rates,” Proc. World Congress on Formal
Methods, p. 1855, 1999.
R. Duke and G. Rose, “Formal Object Oriented Specification Using
Object-Z,” Cornerstones of Computing, Macmillan, 2000.
M.B. Dwyer, G.S. Avrunin, and J.C. Corbett, “Patterns in Property
Specifications for Finite-State Verification,” Proc. 21st Int’l Conf.
Software Eng., pp. 411-420, 1999.
H. Fuhrmann, J. Koch, J. Rennhack, and R.v. Hanxleden, “TheAerospace Demonstrator of DECOS,” Proc. Eighth Int’l IEEE Conf.
Intelligent Transportation Systems, pp. 19-24, 2005.
C. Ghezzi, D. Mandrioli, and A. Morzenti, “Trio: A Logic
Language for Executable Specifications of Real-time System,”J. Systems and Software, vol. 12, no. 2, pp. 107-123, May 1990.
UML Resource Page, Object Management Group, http://
www.omg.org/uml/, 2008.

VOL. 34,

NO. 6,NOVEMBER/DECEMBER 2008[22] V. Gruhn and R. Laue, “Patterns for Timed Property Specifications,” Electronic Notes in Theoretical Computer Science, vol. 153,
no. 2, pp. 117-133, 2006.
[23] L. Grunske, K. Winter, and R. Colvin, “Timed Behavior Trees andTheir Application to Verifying Real-Time Systems,” Proc. 18th
Australian Software Eng. Conf., pp. 211-222, 2007.
[24] D. Harel and E. Grey, “Executable Object Modeling with
Statecharts,” Computer, vol. 30, no. 7, pp. 31-42, July 1997.
[25] K. Havelund, A. Skou, K.G. Larsen, and K. Lund, “Formal
Modeling and Analysis of an Audio/Video Protocol: An
Industrial Case Study Using UPPAAL,” Proc. 18th IEEE Real-Time
Systems Symp., pp. 2-13, 1997.
[26] I.J. Hayes and M. Utting, “Deadlines Are Termination,” Proc. IFIP
Working Conf. Programming Concepts and Methods, 1998.
[27] C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall,1985.
[28] J. Hoenicke and E.-R. Olderog, “Combining Specification Techniques for Processes, Data and Time,” Proc. Third Int’l Conf.
Integrated Formal Methods, pp. 245-266, 2002.
[29] F. Jahanian and A.K. Mok, “A Graph-Theoretic Approach forTiming Analysis and Its Implementation,” IEEE Trans. Computers,
vol. 36, no. 8, pp. 961-975, Aug. 1987.
[30] S. Konrad and B.H.C. Cheng, “Real-Time Specification Patterns,”
Proc. 27th Int’l Conf. Software Eng., pp. 372-381, 2005.
[31] L.M. Lai and P. Watson, “A Case Study in Timed CSP: The
Railroad Crossing Problem,” Proc. Int’l Workshop Hybrid and RealTime Systems, pp. 69-74, 1997.
[32] K.G. Larsen, M. Mikucionis, B. Nielsen, and A. Skou, “Testing
Real-Time Embedded Software Using UPPAAL-TRON: An
Industrial Case Study,” Proc. Fifth ACM Int’l Conf. Embedded
Software, pp. 299-306, 2005.
[33] K.G. Larsen, P. Pettersson, and Y. Wang, “Uppaal in a Nutshell,”Int’l J. Software Tools for Technology Transfer, vol. 1, nos. 1-2,
pp. 134-152, 1997.
[34] M. Lindahl, P. Pettersson, and Y. Wang, “Formal Design andAnalysis of a Gearbox Controller,” Springer Int’l J. Software Tools
for Technology Transfer, vol. 3, no. 3, pp. 353-368, 2001.
[35] N.A. Lynch and F.W. Vaandrager, “Action Transducers andTimed Automata,” Formal Aspects of Computing, vol. 8, no. 5,
pp. 499-538, 1996.
[36] B. Mahony and J.S. Dong, “Timed Communicating Object Z,”
IEEE Trans. Software Eng., vol. 26, no. 2, pp. 150-177, Feb. 2000.
[37] B.P. Mahony and J.S. Dong, “Network Topology and a Case Studyin TCOZ,” Proc. 11th Int’l Conf. Z Users, pp. 308-327, 1998.
[38] J. Ouaknine and J. Worrell, “Timed CSP = Closed Timed EpsilonAutomata,” Nordic J. Computing, vol. 10, no. 2, pp. 99-133, 2003.
[39] A.W. Roscoe, The Theory and Practice of Concurrency. Prentice Hall,
1997.
[40] S. Schneider, Concurrent and Real-Time Systems. John Wiley & Sons,
2000.
[41] J. Sifakis, “The Compositional Specification of Timed Systems—A
Tutorial,” Proc. 11th Int’l Conf. Computer Aided Verification, pp. 2-7,
1999.
[42] J. Sun, J.S. Dong, J. Liu, and H. Wang, “A Formal Object Approachto the Design of ZML,” Annals of Software Eng., vol. 13, pp. 329356, 2002.
[43] J. Woodcock and J. Davies, Using Z: Specification, Refinement, andProof. Prentice Hall, 1996.
Jin Song Dong received the bachelor’s (firstclass honors) and PhD degrees in computing
from the University of Queensland in 1992 and1996, respectively. From 1995 to 1998, he was a
research scientist at the Commonwealth Scientific and Industrial Research Organisation, Australia. Since 1998, he has been with the Schoolof Computing at the National University ofSingapore (NUS), where he is currently an
associate professor and a member of the PhD
supervisors at the NUS Graduate School. He is on the editorial board of
the Formal Aspects of Computing Journal and Innovations in Systems
and Software Engineering, A NASA Journal. His research interests
include formal methods and software engineering. Some of his papers
can be found at http://www.comp.nus.edu.sg/~dongjs.

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.

DONG ET AL.: TIMED AUTOMATA PATTERNSPing Hao received the bachelor’s degree intelecommunication from the Huazhong University of Science and Technology, China, in 2000
and the PhD degree in computer science fromthe National University of Singapore (NUS) in
2008. From 2005 to 2006, she was a research
assistant in the Software Engineering Laboratory, NUS. Her research interests include formal
specification languages, verification, and software engineering. More details about her research and background can be found at http://www.comp.nus.edu.sg/~haoping.
Shengchao Qin received the BSc and PhD
degrees from the School of Mathematical
Sciences, Peking University, in 1997 and 2002,
respectively. He was a research fellow under theSingapore-MIT alliance at the National University of Singapore from July 2002 to December
2004. Since 2005, he has been a lecturer in the
Department of Computer Science at Durham
University, United Kingdom. His research interests include formal methods, programming
languages, and embedded systems. More information about his
research can be found at http://www.dur.ac.uk/shengchao.qin.

859

Jun Sun received the bachelor’s and PhD
degrees from the School of Computing, National
University of Singapore (NUS), in 2002 and2006, respectively. From 2005 to 2006, he was a
research fellow in the School of Computing,
NUS. Since 2006, he has been a Lee Kuan Yew
postdoctoral fellow in the Department of Computer Science, NUS. His research interests aremainly in formal system specification, verification, and synthesis. In particular, he has beenworking with a variety of different specification languages and notations
in order to develop practical tools for elegant system development. Moredetails about his research and background can be found at http://
www.comp.nus.edu.sg/~sunj.
Wang Yi received the PhD degree in computerscience from the Chalmers University of Technology, Sweden, in 1991. He is a professor inreal-time systems at Uppsala University, Sweden, and a Changjiang professor at North
Eastern University, China. From 1991 to 1992,
he was a postdoctoral fellow at Aalborg University, Denmark, before he joined the faculty ofscience and technology at Uppsala University,where he was a lecturer from 1992 to 1994, anassociate professor from 1994 to 2000, and has been a professor since
2000. His interests are mainly in the modeling and verification of
concurrent, distributed, and real-time systems, in particular, techniques
and tools for model-based design, analysis, and implementation ofembedded systems and their industrial applications. He is a cofounderof three software tools for modeling and verification, including UPPAAL,a widely used model checker for timed systems. His publications can befound at http://user.it.uu.se/~yi/.

Authorized licensed use limited to: National University of Singapore. Downloaded on January 24, 2009 at 07:29 from IEEE Xplore. Restrictions apply.