Extending the Real-Time Maude Semantics of Ptolemy to
Hierarchical DE Models
Kyungmin Bae

Peter Csaba Ölveczky

Department of Computer Science
University of Illinois at Urbana-Champaign

Department of Informatics
University of Oslo

This paper extends our Real-Time Maude formalization of the semantics of flat Ptolemy II discreteevent (DE) models to hierarchical models, including modal models. This is a challenging task that
requires combining synchronous fixed-point computations with hierarchical structure. The synthesis
of a Real-Time Maude verification model from a Ptolemy II DE model, and the formal verification of
the synthesized model in Real-Time Maude, have been integrated into Ptolemy II, enabling a modelengineering process that combines the convenience of Ptolemy II DE modeling and simulation with
formal verification in Real-Time Maude.

1

Introduction

One of the most promising approaches to increase the use of formal methods is to enrich the intuitive,
often graphical, informal modeling languages preferred by practitioners with formal analysis capabilities
by: (i) providing a formal semantics to such informal languages, (ii) automatically translating a model
in the informal language into a formal model, and then (iii) verifying the formal model.
For real-time systems, we believe that real-time rewrite theories [19] should be a suitable formalism
in which to define the semantics of time-based modeling languages, for the following reasons:
• Real-time rewrite theories have a natural and “sound” model of timed behavior that makes them
suitable as a semantic framework, and avoids having to prove theorems like “all ill-timed behaviors
can be rearranged into equivalent well-timed behaviors,” as might be needed when using, say, a
timed Petri net semantics (see, e.g., [14] for one such example).
• The expressiveness and generality of real-time rewrite theories allow us to give a formal semantics
to languages with advanced functions and data types, new communication models, arbitrary and
unbounded data structures, program variables ranging over unbounded domains, and so on.
• The associated Real-Time Maude tool [21] provides a range of formal analysis capabilities, including simulation, reachability analysis, and linear temporal logic model checking. Despite the
expressiveness of real-time rewriting, timed-bounded LTL properties are often decidable under
mild conditions [20].
Real-time rewrite theories and Real-Time Maude have been used to define the formal semantics of
– and to provide a simulator and model checker for – some real-time modeling languages, including: a
timed extension of the Actor model [11], the Orc web services orchestration language [3], a language developed at DoCoMo laboratories for handset applications [2], a behavioral subset of the avionics standard
AADL [18], the visual model transformation language e-Motions [22], real-time model transformations
in MOMENT2 [6], and flat Ptolemy II discrete-event models [4].
Ptolemy II [13] is a well established modeling and simulation tool used in industry. A major reason
for its popularity is Ptolemy II’s powerful yet intuitive graphical modeling language that allows a user
P. C. Ölveczky (Ed.): First International Workshop on
Rewriting Techniques for Real-Time Systems (RTRTS’10)
EPTCS 36, 2010, pp. 46–66, doi:10.4204/EPTCS.36.3

c K. Bae and P. C. Ölveczky
This work is licensed under the
Creative Commons Attribution License.

K. Bae and P. C. Ölveczky

47

to build hierarchical models that combine different models of computations. In this paper, we focus on
discrete-event (DE) models, which are explicit about the timing behavior of systems. The Ptolemy II DE
models have a semantics rooted in the fixed-point semantics of synchronous languages [16].
Like many graphical modeling languages, Ptolemy II DE models lack at present formal verification
capabilities. Furthermore, it seems that Ptolemy II DE models fall outside the class of languages which
can be given an automaton-based semantics, because: (i) certain constructs, such as noninterruptible
timers and ramps, require the use of data structures (such as lists) of unbounded size; (ii) the variables
used in, e.g., the transition systems in FSM actors range over infinite domains such as the integers; and
(iii) executing a synchronous step requires fixed-point computations.
In a recent paper [4], we presented a formal semantics for a significant subset of non-hierarchical (or
flat) Ptolemy II DE models. We have used Ptolemy II’s code generation infrastructure to automatically
synthesize a Real-Time Maude verification model from a Ptolemy II model, and have integrated RealTime Maude verification into Ptolemy II, so that Ptolemy II models can be formally analyzed from within
Ptolemy II. This integration of Ptolemy II and Real-Time Maude enables a model-engineering process
that combines the convenience of Ptolemy II modeling with formal verification in Real-Time Maude.
In this paper, we extend and modify the Real-Time Maude semantics of Ptolemy II to the much more
complex transparent hierarchical Ptolemy II DE models, including modal models. We define useful
generic temporal logic propositions for such models, so that a Ptolemy II user can easily define his/her
temporal logic requirements, from within Ptolemy II, without understanding Real-Time Maude or the
formal representation of a Ptolemy II model. We illustrate such formal verification on a hierarchical
fault-tolerant traffic light control system.
Our work on formalizing Ptolemy II is the first attempt to define a Real-Time Maude semantics for
synchronous real-time languages. Apart from the important result of endowing hierarchical Ptolemy
II DE models with formal verification capabilities, the main contribution of this work is to show how
Real-Time Maude can define the formal semantics of synchronous real-time languages with fixed-point
semantics and hierarchical structure. These techniques should be useful for defining the semantics of
other hierarchical synchronous languages. For example, motivated by the complexity-reducing PALS
(physically asynchronous, logically synchronous) architecture pattern [1, 17], which allows us to verify
a synchronous real-time system design while ensuring that the properties also hold for the system’s distributed asynchronous implementation, there is currently an interest in extending the avionics modeling
standard AADL [23] to synchronous behavioral AADL models. Since AADL models are hierarchical,
techniques in this paper could carry over to the definition of a Real-Time Maude semantics of such a
synchronous version of AADL, endowing such AADL models with verification capabilities.
Our work is conducted in the context of the NAOMI project [10], where Lockheed Martin Advanced
Technology Laboratories (LM ATL), UC Berkeley, UIUC, and Vanderbilt University work together to
develop a multi-modeling design methodology. A key part of this project is the systematic use of model
transformations and code generation to maintain consistency across models.
Section 2 introduces Ptolemy II and Real-Time Maude. Section 3 recalls the Real-Time Maude
semantics of flat Ptolemy II DE models described in [4]. Section 4 describes the hierarchical features of
Ptolemy II. Section 5 shows how our semantics for flat models has been extended to hierarchical DE
models. Section 6 presents some useful predefined atomic propositions, allowing users to easily specify
their desired system requirements. Section 7 illustrates Real-Time-Maude-based verification in Ptolemy
II with a hierarchical model of a fault-tolerant traffic light system. Finally, Section 8 presents related work
and gives some concluding remarks. More details about the Real-Time Maude semantics of Ptolemy, as
well as additional verification case studies, are given in the longer technical report [5].

48

Verifying Hierarchical Ptolemy II DE Models

2

Preliminaries on Ptolemy II and Real-Time Maude

2.1

Ptolemy II and its DE Model of Computation

The Ptolemy project1 studies modeling, simulation, and design of concurrent, real-time, embedded systems. The key underlying principle in the project is the use of well-defined models of computation
(MoCs) that govern the interaction between concurrent components. A major problem area being addressed is the use of heterogeneous mixtures of MoCs [13]. A result of the project is a software system
called Ptolemy II, implemented in Java. Ptolemy II allows a user to build hierarchical models that combine different MoCs, including state machines, data flow, and discrete-event models. Models can be
graphically designed and simulated. In addition, Ptolemy II’s code generation capabilities allow models
to be translated into models in other languages or into imperative code, e.g., in C and Java.
A Ptolemy II model is a hierarchical composition of actors with connections between the actors’
input ports and output ports. The actors represent data manipulation units, whose execution is governed
by a special attribute called the director. An essential feature of Ptolemy II is hierarchy: a Ptolemy II
model can itself be treated as an actor, called a composite actor. Ptolemy II also supports modal models,
which are finite state machines where each state of the machine can be refined into an internal model.
Ptolemy II discrete-event (DE) actors consume and produce events at their input and output ports.
An event is a pair (v,t) where v is a value and t is a tag, modeling the time at which the event occurs.
Ptolemy II DE models use super-dense time, in which a tag t is a pair (τ, n) ∈ R≥0 × N, where τ is the
timestamp that indicates the model time when this event occurs, and n is the microstep index.
The semantics of Ptolemy II DE models [15] combines a synchronous-reactive fixed-point iteration
with advancement of time governed by an event queue [16]. Events in that queue are ordered by their
tags. Operation proceeds by iterations, each time removing the event(s) with the smallest tag from the
queue. The removed events are fed to their designated actors. After that, actors with events available
are executed, which may generate new events into the queue. A difference between Ptolemy II and
standard DE simulators is that, at any model time (τ, n), the semantics is defined as the least fixed-point
of a set of equations, similarly to a synchronous model [12]. This allows Ptolemy II models to have
arbitrary feedback loops. Semantics of such models can always be given although they may result in
unknown (bottom) values, in case the model contains causality cycles. Conceptually, the semantics can
be captured by the following pseudo-code:
Q := empty; // Initialize the event queue to be empty.
for each actor A do A.init(); // Initialize A; may generate new events in Q
while Q is not empty do
E := set of all events in Q with the smallest tag;
remove E from Q;
initialize ports with values in E or "unknown";
while port values changed do
for each actor A receiving new values do
A.fire();
// May increase knowledge about presence/absence of inputs at ports
end while;
// Fixed-point reached for the current tag
for each actor A that has been fired do
A.postfire(); // Updates actor state; may generate new events in Q
end while;

1 http://ptolemy.eecs.berkeley.edu/

K. Bae and P. C. Ölveczky

49

Example: A Simple Traffic Light System. Figure 1 shows a Ptolemy DE model of a simple traffic
light system consisting of one car light and one pedestrian light at a pedestrian crossing. Each light is
represented by a set of set variable actors (Pred and Pgrn represent the pedestrian light, and Cred, Cyel,
and Cgrn represent the car light). A light is on iff the corresponding variable has the value 1. The lights
are controlled by two finite state machine (FSM) actors, CarLight and PedestrianLight, that send
values to set the variables; in addition, CarLight sends signals (that are delayed by one time unit) to the
PedestrianLight actor through its Pgo and Pstop output ports.

Figure 1: A simple traffic light model in Ptolemy II.
Figure 2a shows the FSM actor PedestrianLight. This actor has three input ports (Pstop, Pgo,
and Sec), two output ports (Pgrn and Pred), three internal states, and three transitions. This actor reacts
to signals from the car light (by way of the delay actors) by turning the pedestrian lights on and off. For
example, if the actor is in local state Pred and receives input through its Pgo port, then it goes to state
Pgreen, outputs the value 0 through its Pred port, and outputs the value 1 through its Pgrn port.
Figure 2b shows the FSM actor CarLight. Assuming that the clock actor sends a signal every time
unit, we notice, e.g., that one time unit after both the red and yellow car lights are on, these are turned off
and the green car light is turned on by sending the appropriate values to the variables (output: Cred =
0; Cyel = 0; Cgrn = 1). The car light then stays green for two time units before turning yellow.

(a) PedestrianLight

(b) CarLight

Figure 2: The FSM actors for pedestrian lights and car lights.

50

Verifying Hierarchical Ptolemy II DE Models

2.2

Rewriting Logic and Real-Time Maude

A Real-Time Maude timed module specifies a real-time rewrite theory of the form (Σ, E, IR, TR), where:
• (Σ, E) is a membership equational logic [9] theory with Σ a signature2 and E a set of confluent and
terminating conditional equations. (Σ, E) specifies the system’s state space as an algebraic data
type, and must contain a specification of a sort Time modeling the (discrete or dense) time domain.
• IR is a set of (possibly conditional) labeled instantaneous rewrite rules specifying the system’s
instantaneous (i.e., zero-time) local transitions, written rl [l] : t => t 0 , where l is a label. The
rules are applied modulo the equations E.3
• TR is a set of tick (rewrite) rules, written rl [l] : {t} => {t 0 } in time τ, that model time
elapse. {_} is a built-in constructor of sort GlobalSystem, and τ is a term of sort Time that
denotes the duration of the rewrite.
The initial state must be a ground term of sort GlobalSystem and must be reducible to a term of the
form {t} using the equations in the specifications.
The Real-Time Maude syntax is fairly intuitive. For example, function symbols, or operators, are
declared with the syntax op f : s1 . . . sn -> s. f is the name of the operator; s1 . . . sn are the sorts of
the arguments of f ; and s is its (value) sort. Equations are written with syntax eq t = t 0 , and ceq t = t 0
if cond for conditional equations. The mathematical variables in such statements are declared with the
keywords var and vars. We refer to [9] for more details on the syntax of Real-Time Maude.
We use the fact that an equation f (t1 , . . . ,tn ) = t with the owise (for “otherwise”) attribute can be
applied to a subterm f (. . .) only if no other equation with left-hand side f (u1 , . . . , un ) can be applied.4
In object-oriented Real-Time Maude modules, a class declaration
class C | att1 : s1 , ... , attn : sn .

declares a class C with attributes att1 to attn of sorts s1 to sn . An object of class C in a given state is
represented as a term < O : C | att1 : val1 , ..., attn : valn > of sort Object, where O, of sort Oid, is the
object’s identifier, and where val1 to valn are the current values of the attributes att1 to attn . In a concurrent object-oriented system, the state is a term of the sort Configuration. It has the structure of a
multiset made up of objects and messages. Multiset union for configurations is denoted by a juxtaposition operator (empty syntax) that is declared associative and commutative, so that rewriting is multiset
rewriting supported directly in Real-Time Maude. The dynamic behavior of concurrent object systems
is axiomatized by specifying each of its transition patterns by a rewrite rule. For example, the rule
rl [l] : m(O,w)

< O : C | a1 : x, a2 : O’, a3 : z >
=>
< O : C | a1 : x + w, a2 : O’, a3 : z > m’(O’,x) .

defines a family of transitions in which a message m, with parameters O and w, is read and consumed by
an object O of class C. The transitions have the effect of altering the attribute a1 of the object O and of
sending a new message m’(O’,x). “Irrelevant” attributes (such as a3) need not be mentioned in a rule.
A subclass inherits all the attributes and rules of its superclasses.
2 That

is, Σ is a set of declarations of sorts, subsorts, and function symbols.
= E 0 ∪ A, where A is a set of equational axioms such as associativity, commutativity, and identity, so that deduction is
performed modulo A. Operationally, a term is reduced to its E 0 -normal form modulo A before any rewrite rule is applied.
4 A specification with owise equations can be transformed to an equivalent system without such equations [9].
3E

K. Bae and P. C. Ölveczky

51

Formal Analysis. A Real-Time Maude specification is executable, and the tool offers a variety of
formal analysis methods. The rewrite command (trew t in time <= τ .) simulates one behavior
of the system from initial state t up to duration τ. The search command uses a breadth-first strategy
to analyze all possible behaviors of the system, by checking whether a state matching a pattern and
satisfying a condition can be reached from the initial state.
Real-Time Maude also extends Maude’s linear temporal logic model checker to check whether each
behavior, possibly up to a certain time bound, satisfies a temporal logic formula. State propositions are
terms of sort Prop, and their semantics should be given by (possibly conditional) equations of the form
{statePattern} |= prop = b, for b a term of sort Bool, which defines the state proposition prop to hold
in all states {t} where {t} |= prop evaluates to true. A temporal logic formula is constructed by state
propositions and temporal logic operators such as True, False, ~ (negation), /\, \/, -> (implication),
[] (“always”), <> (“eventually”), and U (“until”). The time-bounded model checking command has
syntax (mc t |=t formula in time <= τ .) for initial state t and temporal logic formula formula .

3

Overview of the Formal Semantics of Flat Ptolemy DE Models

This section gives a brief overview of the Real-Time Maude formalization of non-hierarchical and nonmodal (i.e., flat) Ptolemy DE models given in our paper [4]. The reason for including a summary of [4]
is: (i) to convey the main idea of our semantics in a much simpler setting; and (ii) to explain why the
semantics must be significantly changed for the hierarchical case. To avoid introducing too much detail,
we present a slightly simplified version of our semantics, in that we, throughout the paper, assume that
all Ptolemy expressions are constants.

3.1

Representing Flat Ptolemy DE Models in Real-Time Maude

A flat Ptolemy model is represented as an object-oriented Real-Time Maude term
{actors

connections

< global : EventQueue | queue : event queue >}

where actors are objects corresponding to the actor instances in the Ptolemy model; connections are the
connections between the ports of the different actors; and where the value event queue of the queue attribute in the object < global : EventQueue | queue : event queue > denotes the global event queue.
Actors.

Each Ptolemy actor is modeled as an object instance of a subclass of the following class Actor:

class Actor | ports : Configuration,

parameters : ValueMap .

The ports attribute denotes the set of ports of the actor. A port is modeled as an object, as shown below.
The parameters attribute represents the parameters of the corresponding Ptolemy actor, together with
their values, as a semicolon-separated set of terms of the form ’parameter-name |-> value.
A timed delay actor propagates an incoming event after a given time delay. If the delay parameter is
0.0, then there is a “microstep” delay on the generation of the output event. Since the delay parameter is
represented in the parameters attribute of Actor, this subclass does not add any attributes:
class Delay .

subclass Delay < Actor .

A finite state machine (FSM) actor is a transition system containing finite sets of states (or “locations”), local variables, and transitions. A transition has a guard expression, and can contain a set of

52

Verifying Hierarchical Ptolemy II DE Models

output actions and variable assignments. When an FSM actor is fired, Ptolemy assumes that there is at
most one enabled transition. If there is an enabled transition then the actions in the transition are executed. Under the DE director, only one transition step is performed in each iteration. An FSM-Actor is
characterized by its current state, its transitions, and the values of its local variables:
class FSM-Actor | currState : Location,
variables : ValueMap,
subclass FSM-Actor < Actor .

initState : Location,
transitions : TransitionSet .

We model the transitions as a semi-colon-separated set of transitions of the form
s1 --> s2 {guard: g output: pi1|-> ei0 ;. . .; pik |-> ei0 set: v j1 |-> e j0 ;. . .; v jl |-> e j0 }
1

k

1

for state/locations s1 and s2 , port names pi , variables vi , and expressions ei .

l

Ports and Connections. A port is modeled as an object, with a name (the identifier of the object), a
status (unknown, present, or absent), and a value. We have subclasses for input and output ports:
class Port | status : PortStatus, value : Value .
class InPort .
class OutPort .
subclass InPort OutPort < Port .
sort PortStatus .

ops unknown present absent : -> PortStatus [ctor] .

A connection is represented as a term po ==> pi1 ; . . . ; pin of sort Connection, where each p j has the
form a!p for a the name of an actor and p the name of a port. Such a connection connects the output port
po to all the input ports pi1 , . . . , pin Since connections appear in configurations, the sort Connection is
defined to be a subsort of the sort Object.
Global Event Queue. The global event queue is maintained by an object global of class EventQueue
whose queue attribute represents the global event queue as a ::-separated list, ordered according to time
until firing, of terms of the form set of events ; time to fire ; microstep. The set of events is a set of
events, each event characterized by the “global port name” where the generated event should be output
and the corresponding value; time to fire denotes the time until the events are supposed to fire; and
microstep is the additional “microstep” until the event fires.
Example: Representing the Flat Traffic Light Model. The Real-Time Maude representation of the
TimedDelay2 delay actor in the flat non-fault-tolerant traffic light system in Section 2.1 is
< ’TimedDelay2 : Delay | parameters : ’delay |-> # 1.0,
ports : < ’input : InPort | value : # 0, status : absent >
< ’output : OutPort | value : # 0, status : absent >

Likewise, the FSM actor CarLightNormal in the initial state is represented as the

>

term5

< ’CarLight : FSM-Actor | initState : ’Cinit, currState : ’Cinit, variables : ’count |-> # 1,
ports : < ’Sec : InPort | value : # 0, status : absent >
< ’Pgo : OutPort | value : # 0, status : absent > ...,
transitions : (’Cinit --> ’Cred
{guard: (# true)
output: (’Cred |-> # 1) ; (’Cyel |-> # 0) ; (’Cgrn |-> # 0)
set: ’count |-> # 0}) ;
(’Cred --> ’Cred
{guard: (isPresent(’Sec) && (’count lessThan # 2))
output: emptyMap
set: ’count |-> (’count + # 1)}) ; ... > .
5 To

save space, some terms are replaced by ‘...’

K. Bae and P. C. Ölveczky

53

The connection from the output port output of the Clock actor to the input port Sec of CarLight
and the input port Sec of PedestrianLight is represented by the term
(’Clock !’output) ==> (’PedestrianLight ! ’Sec) ; (’CarLight ! ’Sec)

3.2

Specifying the Behavior of Flat DE Models

As explained in Section 2.1, the behavior of Ptolemy DE models can be summarized as repeatedly:
• Advance time until the time to fire the first events in the queue is (0, 0).
• And then perform an iteration of the system. That is:
1. The events that are supposed to fire are added to the corresponding output ports; the status
of all other ports is set to unknown.
2. (Fire) Then the fixed point of all ports is computed by gradually increasing the knowledge
about the presence/absence of inputs to and output from ports until a fixed-point is reached.
3. (Postfire) Finally, states are updated for actors with inputs or scheduled events, and new
events are generated and inserted into the event queue.
The following tick rule advances time until the time when the first events in the event queue are
scheduled (we first declare all the variables used):
vars SYSTEM OBJECTS PORTS PORTS’ REST REST2 IA ACTS : ObjectConfiguration . var N : Nat .
var EVTS : Events . var QUEUE : EventQueue . vars V TV : Value . vars PARAMS : ValueMap .
vars T T’ : Time . var NZT : NzTime . vars STATE STATE’ : Location . vars O O’ CO : Oid .
var CF : Configuration . var BODY : TransBody . var TRANSSET : TransitionSet .
vars P P’ : PortId . var EPIS : EportIdSet . var PS : PortStatus . var NZ : NzNat .
rl [tick] :
{SYSTEM < global : EventQueue | queue : (EVTS ; NZT ; N) :: QUEUE >}
=>
{delta(SYSTEM, NZT)
< global : EventQueue | queue : (EVTS ; 0 ; N) :: delta(QUEUE, NZT) >}

in time NZT .

The first event(s) in the event queue have non-zero delay NZT. Time is advanced by this amount NZT, and,
as a consequence, the (first component of the) event timer goes to zero. In addition, the function delta
is applied to all the other objects (denoted by SYSTEM) in the system. The function delta defines the
effect of time elapse on the objects. This function is also applied to the other elements in the event queue,
where it decreases the remaining time of each event set by the elapsed time NZT (see [4] for details).
The “microstep tick rule” that advances “time” by microsteps is not shown. When the remaining
time and microsteps of the first events in the queue are both zero, an iteration of the system is performed:
rl [executeStep] :
{SYSTEM < global : EventQueue | queue : (EVTS ; 0 ; 0) :: QUEUE >}
=>
{< global : EventQueue | queue : QUEUE >
postfire(portFixPoints(addEventsToPorts(EVTS, clearPorts(SYSTEM))))} .

The function clearPorts sets the status of each port to unknown. The operator addEventsToPorts
inserts the events scheduled to fire into the corresponding output ports. The portFixPoints function
then finds the fixed points for all ports (fire), and postfire “executes” the steps on the computed port
fixed-points by changing the states of the objects and generating new events and inserting them into the
global event queue. These functions have sort Configuration, whereas the equations defining them
involve variables of the subsort ObjectConfiguration, so that each function has finished computing
before the “next” function is computed:

54

Verifying Hierarchical Ptolemy II DE Models

ops clearPorts portFixPoints postfire : Configuration ~> Configuration .

To completely define the behavior of a system, we must define clearPorts, portFixPoints, and
postfire on the different actors.
Computing the Fixed-Point for Ports. The idea behind the function portFixPoints, that computes
the fixed-point for all ports, is simple. The state has the form portFixPoints(actors and connections),
where initially, the only port information are the events scheduled for this iteration. For each case when
the status of an unknown port can be determined to be either present or absent, there is an equation
eq portFixPoints(< O : ... | ports : < P : Port | status : unknown > PORTS, ... >
connections and other objects)
= portFixPoints(< O : ... | ports : < P : Port | status : present, value : ... > PORTS, ... >
connections and other objects) .

(and similarly for deciding that input/output is absent). The fixed-point is reached when no such equation can be applied. The portFixPoints operator is then removed by using the owise construct:
eq portFixPoints(OBJECTS) = OBJECTS [owise] .

The following equation propagates port status from a “known” output port to a connecting unknown
input port. The present/absent status (and possibly the value) of the output port P of actor O is propagated to the input port P’ of the actor O’ through the connection (O ! P) ==> ((O’ ! P’) ; EPIS):
ceq portFixPoints(
< O : Actor | ports : < P : OutPort | status : PS , value : V > PORTS >
((O ! P) ==> ((O’ ! P’) ; EPIS))
< O’ : Actor | ports : < P’ : InPort | status : unknown > PORTS’ >
REST)
= portFixPoints(< O : Actor | > ((O ! P) ==> ((O’ ! P’) ; EPIS))
< O’ : Actor | ports : < P’ : InPort | status : PS, value : V > PORTS’ >
REST)
if PS =/= unknown .

The portFixPoints function must then be defined for each kind of actor to decide whether the actor
produces any output in a given port. For example, the timed delay actor does not produce any output in
this iteration as a result of any input. Therefore, if its status is unknown (that is, the delay actor did not
schedule an event for this iteration), its output port should be set to absent:
eq portFixPoints(< O : Delay | ports : < P : OutPort | status : unknown > PORTS > REST)
= portFixPoints(< O : Delay | ports : < P : OutPort | status : absent > PORTS > REST) .

The definition of portFixPoints for FSM actors relies on the assumption that at most one transition
is enabled at any time. In the following conditional equation, one transition from the current state STATE
is enabled. In addition, there is some input to the actor (through input port P’), and some output ports
have status unknown. The function updateOutPorts then updates the status and the values of the output
ports according to the current state and input:
ceq portFixPoints(< O : FSM-Actor | ports : < P’ : InPort | status : present >
< P : OutPort | status : unknown > PORTS,
currState : STATE, parameters : PARAMS,
transitions : (STATE --> STATE’ {BODY}) ; TRANSSET >
REST)
= portFixPoints(< O : FSM-Actor | ports : updateOutPorts(PARAMS, BODY,
< P : OutPort | > < P’ : InPort | > PORTS) >
REST)
if transApplicable(< P : OutPort | > < P’ : InPort | > PORTS, PARAMS, BODY) .

K. Bae and P. C. Ölveczky

55

Another equation sets all output ports to absent if there is enough information to determine that no
transition can become enabled in the current round.
Postfire. The postfire function distributes over the actor objects in the configuration and updates
internal states and generates new events that are inserted into the event queue. An owise equation defines
postfire to be the identity function on those actors that do not have other equations defining postfire.
If a delay actor has input in its ’input port, then it generates an event with a delay equal to the value
of the ’delay parameter. If this delay is 0.0, the microstep is 1, otherwise the microstep is 0. This event
is added to the global event queue using the addEvent function that adds the new event to the queue:
eq postfire(< O : Delay | ports : < ’input : InPort | status : present, value : V >
< ’output : OutPort | >,
parameters : ’delay |-> TV ; PARAMS >)
< global : EventQueue | queue : QUEUE >
=
< O : Delay | >
< global : EventQueue | queue : addEvent(event(O ! ’output, V), toTime(TV),
if toTime(TV) == 0 then 1 else 0 fi, QUEUE) > .

An FSM actor does not generate future events, but postfire updates the location and variables of
the actor if it has input and has an enabled transition; again, the rule is given in [4].

4

Hierarchical Ptolemy DE Models

Ptolemy II hierarchical models contain components (or actors) that are themselves Ptolemy II models.
Such a hierarchical model can again be encapsulated and be seen as a single composite actor (Noncomposite actors are called atomic actors). An inner actor of a DE composite actor is executed if that
inner actor receives some events at its input ports. Ptolemy II also provides modal models where several
sub-models are controlled by a state machine. Each “state” of a modal model is (or “refines to”) a
Ptolemy model, and only the model of the current state is executed during the computation step.
Composite Actors. Composite actors can have parameters, ports to communicate with other actors,
and a sub-model that can be any Ptolemy model. The ports of a composite actor are connected to its
inner actors so that the sub-model interacts with the outside. The input ports of composite actors are
connected to the input ports of inner actors, and the output ports of composite actors are connected to the
output ports of inner actors. Figure 3 illustrates a hierarchical composition of actors.

A0

A3

A4

A1

A6
A5

A7

A2

Figure 3: A hierarchical composition of actors. A0–A7 are actors, and A0 and A3 are composite actors.

56

Verifying Hierarchical Ptolemy II DE Models

In Ptolemy II, each composite actor can have its own director to support heterogeneous modeling. If
the director of a composite actor is the same as the director of the parent actor, it is called a transparent
actor. In this paper, we consider only transparent cases since we verify DE models. The evaluation order
of actors in a transparent hierarchical model is essentially the same as in the flat case. A composite
actor is fired if a new value has arrived to an input port of the actor, and the value is transferred to the
ports connected to the input port. If an output port of a composite actor gets a new value, either from
inner actors or from input ports of the actor, the value is transferred to the connected ports. This port
fixed-point computation finishes when no other port-transfer is available, just as in the flat case.
Modal Models. Modal models are finite state machines where each state has a refinement actor, which
is either a composite actor or an FSM actor. The input and output ports of the refinements are the same
as those of the modal model. In the top level of a modal model, the output ports are regarded as both
input and output ports so that the transitions of modal models may use the evaluation result of refinement
actors in the current computation step. The left-hand side of Fig. 4 shows a modal model with two states.

P3

P1
S0

S1

S0

S1

Controller

P2

ModalModel

P1

P3

P1

S0
P2

S0

P3

S1

S1

P2

CompositeActor

Figure 4: A modal model with 2 states and its equivalent representation as a composite actor. S0 and S1
are states, triangles are ports, and diamonds are input/output ports. Dashed lines are connections, and a
solid line in the right-hand side means a coupled input/output ports.
When a modal model fires, the refinement of the current state is fired and the other refinements
are frozen. The guards of all outgoing transitions from the current state of the modal model are then
evaluated.6 If exactly one of those guards is true, then the transition is taken and the actions on the
transition are executed. If more than one of the guards is true, then it is considered as an error in Ptolemy
II. The refinement of the next state will be executed in the next computation step. In case of a conflict
between the refinements and the parent actor, the latter overwhelms the former. For example, if the FSM
controller of a modal model and the refinement of a current state are trying to write different values to
the same output port, then the value of the FSM controller is taken.
A modal model can be seen as syntactic sugar for a composite actor with frozen inner actors, as
shown in Fig. 4, where the right-hand side shows the equivalent composite-actor representation of the
modal model in the left-hand side. That is, a modal model A is semantically equivalent to a composite
actor Ã, with the same ports, that has the controller FSM actor and the refinement actors as inner actors,
so that: (i) the ports are connected as indicated in Fig. 4; (ii) the controller FSM actor is fired after the
refinement actors are fired; (iii) only the refinement inner actors corresponding to the current state of the
controller are evaluated, whereas the other refinement actors are frozen, in the sense that their states do
6

Both the input ports and the input/output ports of modal models can be used here.

K. Bae and P. C. Ölveczky

57

not evolve and the values of their outports are ignored; and (iv) if an output port of the controller FSM
actor has no value but its coupled input port has some value, then the output port will have the same
value as the input port. Our Real-Time Maude semantics in Section 5 follows this semantics.

5

Real-Time Maude Semantics for Hierarchical DE Models

We define the Real-Time Maude semantics for hierarchical DE models by extending our semantics for
flat models to composite actors and modal models, and by making some changes to the flat semantics as
described below. Our Real-Time Maude representation preserves the hierarchical structure of a Ptolemy
II model; therefore such models and their Real-Time Maude counterparts are essentially isomorphic, so
that we can easily reconstruct the original Ptolemy II models to provide graphical counter-examples.
Some of the difficulties involved in extending the semantics to the hierarchical case include:
• The event management is different. DE models have a global event queue, but events could be
generated at any level and may need to be delivered deep down in the hierarchy.
• Computing fixed-points for hierarchical models is much harder than in the flat case. Naive approaches easily fall into infinite loops or unnecessarily complex semantics. In addition, the fixedpoint computation should be finished only after all levels of fixed-point computation are completed.
• The semantics of modal models in the Ptolemy II documentation is somewhat unclear. There
are many subtle or implicit assumptions concerning the execution of modal models, such as the
evaluation order of inner actors, event generation in frozen actors, and handling input/output ports
of modal models. We proposed the transformation from modal models to composite actors for
clarifying the semantics of modal models, and have discussed this issue extensively with members
of the Ptolemy team.

5.1

Representing Hierarchical Actors

Composite actors are modeled as object instances of the class CompositeActor, which extends its superclass Actor with one attribute, innerActors, which denotes the inner actor objects and connections
of the composite actor:
class CompositeActor | innerActors : Configuration .
subclass CompositeActor < Actor .

We also add the following new class AtomicActor, and declare each atomic actor class to be a
subclass of AtomicActor.
class AtomicActor .

subclass AtomicActor < Actor .

Each actor can be uniquely identified by its global actor identifier, which is a list o1 . o2 . . . . . on
of object names, where o1 is the name a top-level actor, and which includes all identifiers of composite
actors containing the given actor.
We represent modal models as composite actors according to the frozen-composite-actor semantics
for modal models described in Section 4. The class ModalModel has an additional attribute controller
pointing to the controller FSM in innerActors, and the additional refinementSet attribute mapping
each state in the modal model to its refinement:
class ModalModel | controller : Oid, refinement : RefinementSet .
subclass ModalModel < CompositeActor .

58

Verifying Hierarchical Ptolemy II DE Models

In addition, the definition of the basic Actor class adds an attribute status which can have the value
enabled or disabled to reflect that any actor may be disabled as a result of being contained in a refinement of a state in a modal model which is “frozen.” The equations for postfire and portFixPoints
generating a value at outports only apply to objects whose status is enabled. The other equations such
as clearPorts are applied to disabled actors.

5.2

Extracting and Adding Event to the Event Queue

In the flat setting, each actor is at the same hierarchical level as the global EventQueue object. Each
actor therefore has direct access to the event queue, so that at the start of an iteration, the scheduled events
could be directly inserted into the corresponding actor ports (by the function addEventsToPorts), and
actors could add generated events directly into the global event queue (by postfire).
In the hierarchical case, an actor that receives or generates an event from/to the global event queue
can be located deep down in the actor hierarchy. Events communicated between the actors and the
event queue may therefore cross hierarchical boundaries. We have modeled this “traveling” of events
by “method calls” or “messages”. For example, inserting an event into the output port p of some actor
with global actor identifier g corresponds to generating the message active-evt(event(g ! p, v)).
Likewise, an event generated by an actor is “sent” to the event queue as a “message” of the form
schedule-evt(event, time, microstep):
msg schedule-evt : Event Time Nat -> Msg .
msg active-evt : Event -> Msg .

For example, when an actor generates an event, it creates a schedule-evt “message”:
eq postfire(< O : Delay | status : enabled, parameters : ’delay |-> TV ; PARAMS,
ports : < ’input : InPort | status : present, value : V >
< ’output : OutPort | > PORTS >)
= schedule-evt(event(O ! ’output, V), toTime(TV), if toTime(TV) == 0 then 1 else 0 fi)
< O : Delay | > .

Such an event is propagated towards the top of the actor hierarchy by the following equation, in which
a composite actor inside whose innerActors the schedule-evt message resides moves the message
one level up:
eq < O : CompositeActor | innerActors : CF schedule-evt(event(AI ! PI, V), T, N) >
= < O : CompositeActor | innerActors : CF >
schedule-evt(event((O . AI) ! PI, V), T, N) .

When the schedule-evt request has reached the top of the hierarchy, it is added to the event queue:
eq < global : EventQueue | queue : QUEUE > schedule-evt(EVENT, T, N)
= < global : EventQueue | queue : addEvent(EVENT, T, N, QUEUE) > .

The propagation of active-evts from the event queue to some inner actor is explained below.
The rewrite rule executeStep that models an iteration of the system is modified w.r.t. the flat case,
so that for each event event(globalActorId ! portId, v) scheduled for this iteration (i.e., included in
EVTS below), a “message” active-evt(event(globalActorId ! portId, v)) is added to the state; the
function releaseEvt generates this message set from a set of events:
rl [executeStep] :
{SYSTEM < global : EventQueue | queue : (EVTS ; 0 ; 0) :: QUEUE >}
=>
{< global : EventQueue | queue : QUEUE >
postfire(portFixPoints(releaseEvt(EVTS) clearPorts(SYSTEM)))} .

K. Bae and P. C. Ölveczky

5.3

59

Defining clearPorts, portFixPoints, and postfire for Hierarchical Models

For atomic actors, clearPorts should just set the status of each port of the actor to unknown, as
before. For composite actors, it should also propagate to the inner actors. To ensure that the appropriate
equation applies to an actor, we must modify the definition of clearPorts for atomic actors to apply
only to objects of class AtomicActor:
eq
=
eq
=

clearPorts(< O : AtomicActor | ports : PORTS >)
< O : AtomicActor | ports : clearPorts(PORTS) > .
clearPorts(< O : CompositeActor | innerActors : CF, ports : PORTS >)
< O : CompositeActor | innerActors : clearPorts (CF), ports : clearPorts(PORTS) > .

The postfire function is almost unchanged for the “flat” actors; the only modification is to ensure
that postFire is not applied to disabled actors, since disabled actors should not change their states or
generate new events. For a composite actor, postfire just propagates to its inner actors. The condition
ensures that this equation is not applied to modal models:
ceq postfire(< O : CompositeActor | status : ST, innerActors : CF >)
= < O : CompositeActor | innerActors : if ST == enabled then postfire (CF) else CF fi >)
if class(< O : CompositeActor | >) == CompositeActor .

The extension of the portFixPoints function to the hierarchical case is more subtle due to repeated
computations. The portFixPoints function should distribute to the submodels of composite actors, to
compute the fixed points of these subsystems. However, an equation of the form
eq portFixPoints(< O : CompositeActor | innerActors : IA, ... > REST)
= portFixPoints(< O : CompositeActor | innerActors : portFixPoints(IA), ... > REST) .

would be applicable again when the inner portFixPoints function disappears, leading to nontermination (and non-applicability of the owise equation defining the end of the fixed-point computation). This
anomaly is actually caused by applying portFixPoints to inner actors even though they may already
have reached their fixed points. To avoid this situation, we need to execute portFixPoints for inner
actors only if some inner actors have not yet reached a fixed-point. This can be easily accomplished
since actors are activated in DE models only if input ports of the actors receive some value either from
the event queue or from the other actors by connections.
We therefore start the fixed-point computation of inner actors in the portFixPoints function of
composite actors for the following cases:
1. Some events from the global event queue are passed to some inner actors.
2. An input port of a composite actor connected to some inner actors receives some value.
For Case 1, when released events in a configuration should be propagated to some inner actor of
a composite actor, we begin the portFixPoints computation of those inner actors. The following
equations describe the propagation of active-evts from the event queue to inner actors. If there are
some events toward an inner actor of a composite actor, all such events are then passed to the inner actors
and portFixPoints of the inner actors is started. This equation is the only equation defined on the sort
Configuration so that it is executed first before the other fixed-point equations are evaluated:
ceq portFixPoints(active-evt(event((O . AI) ! PI, V))
< O : CompositeActor | innerActors : ACTS > CF)
= portFixPoints(< O : CompositeActor | innerActors : portFixPoints (MSGS ACTS) > CF’)
if fr(MSGS, CF’) := filterMsg(O, CF, active-evt(event(AI ! PI, V)) ) .

60

Verifying Hierarchical Ptolemy II DE Models

The function filterMsg separates the events toward inside from the others, and returns a constructor
fr(Events,Conf ) which is a pair of the desired events and the other configuration.
In Case 2, we must define the portFixPoints function for the port-propagation of composite actors.
An input to a composite actor will lead to an input to one of its subactors, and an output at a subactor will
lead to an output from the containing composite actor (the special name ‘parent’ denotes the containing
actor of an actor in port names). When a composite actor passes a value (or the knowledge that input will
be absent) to inner actors, if the inner fixed-point computation has not started yet or is already finished,
then portFixPoints must again be called to (re-) compute the fixed-point of the inner diagram:
ceq portFixPoints(
< O : CompositeActor |
status : enabled ,
ports : < P : InPort | status : PS, value : V > PORTS,
innerActors :
(parent ! P) ==> (O’ ! P’ ; EPIS)
< O’ : Actor | ports : < P’ : InPort | status : unknown > PORTS2 >
REST2 >
REST)
=
portFixPoints(
< O : CompositeActor |
innerActors : portFixPoints(
*** (re-) start the inner fixed-point
(parent ! P) ==> (O’ ! P’ ; EPIS)
< O’ : Actor | ports : < P’ : InPort | status : PS , value : V > PORTS2 >
REST2) >
REST) if PS =/= unknown .

Of course, a composite actor can pass an updated port status/value to its inner actors also when those
inner actors are already computing portFixPoints; that case is modeled by an equation that is very
similar to the above equation and is not shown.
Likewise, an inner actor can propagate the status of output ports to the containing actor. In this case,
we only consider when the inner fixed-point is already finished, because in Ptolemy II an inner actor has
a higher priority than a parent actor in the evaluation order:
ceq portFixPoints(
< O : CompositeActor |
ports : < P : OutPort | status : unknown > PORTS,
innerActors :
(O’ ! P’) ==> (parent ! P ; EPIS)
< O’ : Actor | status : enabled ,
ports : < P’ : OutPort | status : PS, value : V > PORTS2 >
REST2 >
REST)
=
portFixPoints(
< O : CompositeActor |
ports : < P : OutPort | status : PS, value : V > PORTS,
innerActors : (O’ ! P’) ==> (parent ! P ; EPIS)
< O’ : Actor | ports : < P’ : OutPort | > PORTS2 >
REST2 >
REST) if PS =/= unknown .

K. Bae and P. C. Ölveczky

61

An owise equation is again used to end the fixed-point computation when no equation adding new information about the ports can be applied. However, to end the fixed-point computation of a (sub)system,
the fixed-point computations of the subsystems of composite actors must have finished. Therefore, this
owise equation should only be applied when there is no portFixPoints operator in the innerActors
of the CompositeActors in the system. Since portFixPoints is declared as a partial function, no object with an occurrence portFixPoint operator somewhere in its inner actors (or in some subactor of an
inner actor) will be a term of sort Object. That is, actors of sort Object do not contain portFixPoints:
ceq portFixPoints(OBJECTS) = OBJECTS [owise] .

Modal Models. Most of the semantics for modal models is borrowed from the semantics of composite
actors, except for frozen actors, coupled ports, and the evaluation order between the controller and refinements. For modal models, postfire also sets the status attribute of the inner actors according to
the current state of the controller to freeze all refinement actors except the refinement of the current state:
eq postfire(
< O : ModalModel | status : enabled, controller : CO, refinement : REFS,
innerActors : CF >)
=
< O : ModalModel | innerActors : (< CO : FSM-Actor | >
setStateRefinement(STATE, REFS, ACTS)) >
if < CO : FSM-Actor | currStatus : STATE > ACTS := postfire(CF) .

The function setStateRefinement disables all refinements except the refinement of the current state.
If the controller depends on the result of portFixpoints of some refinement actors, then the result
must be transferred through some coupled input port of the controller actor. Hence the evaluation order
between the controller and refinements is automatically treated in our representation. The only part not
yet covered is to handle coupled input/output ports in the controller FSM actor of a modal model. In our
representation, the coupled input/output ports have the same name, and the value of the input port will
be copied only if the coupled output port is absent:
eq portFixPoints(
< O : ModalModel | status : enabled , controller : CO,
innerActors :
< CO : FSM-Actor | status : enabled ,
ports : < P : InPort | status : present , value : V >
< P : OutPort | status : absent > PORTS >
REST2 >
REST)
=
portFixPoints(
< O : ModalModel | innerActors : portFixPoints(
< CO : FSM-Actor |
ports : < P : InPort | >
< P : OutPort | status : present, value : V > PORTS >
REST2 >)
REST) .

The above equation can be only applied after the inner fixed-point computation triggered by the controller
FSM actor has been finished. Therefore, an output port copies a value from its coupled input port only if
no value is generated at the output port when the controller is computed.

62

Verifying Hierarchical Ptolemy II DE Models

However, because of the above equation, the absent status of coupled output ports should not be
transferred to the parent until we can decide whether the associated coupled input port is absent or
not. For this reason we do not explicitly represent the connections between coupled output ports of the
controller and the output ports of the parent modal model. Instead, we define the following equations to
propagate the value of the coupled output ports:
eq portFixPoints(
< O : ModalModel | status : enabled, controller : CO,
ports : < PI : OutPort | status : unknown > PORTS,
innerActors : < CO : FSM-Actor | ports :
< PI : OutPort | status : present , value : V > PORTS’ >
ACTS >
REST)
=
portFixPoints(
< O : ModalModel | ports : < PI : OutPort | status : present , value : V > PORTS >
REST) .

The absent status of a coupled output port is propagated only if the associated input port is also absent:
eq portFixPoints(
< O : ModalModel | status : enabled, controller : CO,
ports : < PI : OutPort | status : unknown > PORTS,
innerActors :
< CO : FSM-Actor |
ports : < PI : InPort | status : absent >
< PI : OutPort | status : absent > PORTS’ >
ACTS >
REST)
=
portFixPoints(
< O : ModalModel | ports : < PI : OutPort | status : absent > PORTS > REST) .

6

Specifying Temporal Logic Properties in Hierarchical Models

In Real-Time Maude, an LTL formula is constructed from a set of (possibly parametric) atomic state
propositions and the usual Boolean and LTL operators. Having to define atomic state propositions makes
the verification process nontrivial for the Ptolemy user, since it requires some knowledge of the RealTime Maude representation of the Ptolemy model, as well as the ability to define functions in Real-Time
Maude. To free the user from this burden, we have predefined some generic atomic propositions, which
extend the ones for flat Ptolemy models in [4]. For example, the property
actorId | var1 = value1 , . . . , varn = valuen
holds in a state if the value of parameter vari of an actor equals valuei for each 1 ≤ i ≤ n, where actorId
is the global actor identifier of a given actor. For FSM actors, the property
actorId @ location
holds if and only if the FSM actor with global name actorId is in location (or “local state”) location.

K. Bae and P. C. Ölveczky

63

An LTL formula may contain multiple occurrences of the above atomic propositions. To avoid having
to unnecessarily write long global actor names too many times, we can simplify a formula for inner actors
with an actor scope, so that
actorId : formula
denotes that formula should hold in the actor with the global identifier actorId. For example, the formula
o1 . o2 : [] (o3 @ l1 /\ o4 . o5 @ l2 ) equals the formula [] (o1 . o2 . o3 @ l1 /\ o1 . o2 . o4 . o5 @ l2 ).

7

Example: A Fault-Tolerant Hierarchical Traffic Light

This section shows how a hierarchical Ptolemy II DE model, that specifies a fault-tolerant traffic light
system at a pedestrian crossing, can be verified from within Ptolemy using Real-Time Maude. The
Ptolemy II model is taken from [7]. The system consist of one car light and one pedestrian light.
Figure 5 shows the system. The FSM actor Decision “generates” failures and repairs by alternating
between staying in location Normal for 15 time units and staying in location Abnormal for 5 time units.
Whenever the actor takes a transition with target Normal, it sends a signal through its Ok port, and
whenever it reaches, or stays in, location Abnormal, the actor sends a signal through its Error port.
TrafficLight is a modal model handling the two lights; whenever it is in error mode and receives a
signal through its Ok port, the actor goes to normal mode, and vice versa when it receives an Error event
in normal mode. The FSM actor that refines the error mode of TrafficLight has three states. In this
mode, all lights are turned off (by sending a value 0 through the corresponding port), except for the yellow
light of the car light, which is blinking. The refinement of the normal mode in TrafficLight is the
composite actor that consists of the two FSM actors CarLight and PedestrianLight, that define the
behavior of the two lights during normal operations, and that have already been explained in Section 2.1.
As before, Pred, Pgrn, Cred, Cyel, and Cgrn are variables that denote the current color(s) (if any) of
the lights. Finally, the actor Clock produces a signal every time unit.
As explained in [4], we have used Ptolemy’s code generation infrastructure to integrate both the
synthesis of a Real-Time Maude model from a Ptolemy II model, and the verification of the generated
Real-Time Maude model, into Ptolemy II. Figure 6 shows the dialog box that appears when the user
double clicks on the blue RTMaudeCodeGenerator button in Ptolemy II DE models. This dialog box
allows the user to write his/her model checking commands, and then displays both the generated RealTime Maude code and the results of the verification when the user presses the ’Generate’ button.
The main safety property is that the car light and the pedestrian light never show green at the same
time. That is, the variable Pgrn and the variable Cgrn should never be 1 at the same time, which, assuming that the entire model is called HierarchicalTrafficLight, can be defined as the LTL formula
[] ~ (’HierarchicalTrafficLight | (’Pgrn = # 1, ’Cgrn = # 1) )

We can also specify the safety of the traffic light controller. If the traffic light is in normal mode, the
CarLightNormal FSM actor should not be in state Cgrn when the pedestrian light is in state Pgreen:
’HierarchicalTrafficLight : (
[] (’TrafficLight @ ’normal ->
~ (’TrafficLight . ’normal : (’CarLight @ ’Cgrn /\ ’PedestrianLight @ ’Pgreen))))

We can also check the liveness property that both pedestrian and cars can cross infinitely often. That
is, it is infinitely often the case the pedestrian light is green when the car light is not green, and it also
infinitely often the case the car light is green when the pedestrian light is not green:
[]<> (’HierarchicalTrafficLight | (’Pgrn = # 1, ’Cgrn = # 0))
/\ []<> (’HierarchicalTrafficLight | (’Pgrn = # 0, ’Cgrn = # 1))

64

Verifying Hierarchical Ptolemy II DE Models

HierarchicalTrafficLight

TrafficLight
Decision
TrafficLight

Normal
Error

Figure 5: A hierarchical fault-tolerant traffic light system.

8

Related Work and Concluding Remarks

A preliminary exploration of translations of synchronous reactive (i.e., untimed) Ptolemy II models into
Kripke structures, that can be analyzed by the NuSMV model checker, and of DE models into communicating timed automata is given in [8]. However, they require data abstraction to map models into
finitary automata, and they flatten hierarchical models. On the other hand, as mentioned in the introduction, Real-Time Maude has been used to define the semantics of several real-time languages, but we
are not aware of any translation of a synchronous and hierarchical real-time language into Maude or
Real-Time Maude. The semantics of non-hierarchical Ptolemy II DE models is described in the recent
paper [4] that we extend to hierarchical models in this paper.
We have shown how the Real-Time Maude formalization of the semantics for flat Ptolemy II DE
models has been extended to the hierarchical case. Combining a fixed-point synchronous semantics with
hierarchical structure is not entirely trivial, as we explain in Section 5. An additional benefit of our work

K. Bae and P. C. Ölveczky

65

Figure 6: The dialog box for the Ptolemy II verification
is the clarification of the semantics of modal models, for which we have also given a composite-actor
semantics in Ptolemy II.
We have integrated Real-Time Maude code generation and model checking of hierarchical DE models into Ptolemy II, enabling a model-engineering process for embedded systems that leverages the convenience of Ptolemy II DE modeling and simulation with the formal verification of Real-Time Maude.
Acknowledgments. This work is part of the Lockheed Martin Advanced Technology Laboratories’ NAOMI
project. We thank the members of the NAOMI project for enabling and encouraging this research; Christopher
Brooks, Chihhong Patrick Cheng, Thomas Huining Feng, Edward A. Lee, Man-Kit Leung, and Stavros Tripakis
for discussions on Ptolemy II; José Meseguer for encouraging us to study the formal semantics of Ptolemy in
Real-Time Maude; and the anonymous reviewers for many helpful comments on an earlier version of this paper.
We gratefully acknowledge financial support by Lockheed Martin Corporation, through the NAOMI project, The
Research Council of Norway, through the Rhytm project, and NSF Grant CNS 08-34709.

References
[1] A. Al-Nayeem, Mu Sun, X. Qiu, L. Sha, S. P. Miller & D. D. Cofer (2009): A Formal Architecture Pattern
for Real-Time Distributed Systems. In: Proc. 30th IEEE Real-Time Systems Symposium, IEEE.
[2] M. AlTurki, D. Dhurjati, D. Yu, A. Chander & H. Inamura (2009): Formal Specification and Analysis of
Timing Properties in Software Systems. In: FASE’09, Lecture Notes in Computer Science 5503, Springer,
pp. 262–277.
[3] M. AlTurki & J. Meseguer (2007): Real-time rewriting semantics of Orc. In: Michael Leuschel & Andreas
Podelski, editors: Proc. PPDP’07, ACM.

66

Verifying Hierarchical Ptolemy II DE Models

[4] K. Bae, P. C. Ölveczky, T. H. Feng & S. Tripakis (2009): Verifying Ptolemy II Discrete-Event Models Using
Real-Time Maude. In: ICFEM’09, Lecture Notes in Computer Science 5885, Springer, pp. 717–736.
[5] K. Bae, P. C. Ölveczky, T. H. Feng & S. Tripakis (2009): Verifying Ptolemy II Discrete-Event Models using
Real-Time Maude. Manuscript, http://www.ifi.uio.no/RealTimeMaude/Ptolemy.
[6] A. Boronat & P. C. Ölveczky (2010): Formal Real-Time Model Transformations in MOMENT2. In: FASE,
Lecture Notes in Computer Science 6013, Springer, pp. 29–43.
[7] C. Brooks, T. H. Feng, E. A. Lee & R. von Hanxleden (2008): Multimodeling: A Preliminary Case Study.
Technical Report UCB/EECS-2008-7, EECS Department, University of California, Berkeley.
[8] C. P. Cheng, T. Fristoe & E. A. Lee (2008): Applied Verification: The Ptolemy Approach. Technical Report
UCB/EECS-2008-41, EECS Department, University of California, Berkeley.
[9] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martı́-Oliet, J. Meseguer & C. Talcott (2007): All About Maude
- A High-Performance Logical Framework, Lecture Notes in Computer Science 4350. Springer.
[10] T. Denton, E. Jones, S. Srinivasan, K. Owens & R. W. Buskens (2008): NAOMI – An Experimental Platform
for Multi-modeling. In: MoDELS’08, Lecture Notes in Computer Science 5301, Springer, pp. 143–157.
[11] H. Ding, C. Zheng, G. Agha & L. Sha (2003): Automated Verification of the Dependability of Object-Oriented
Real-Time Systems. In: Proc. WORDS’03, IEEE Computer Society Press.
[12] S. Edwards & E. Lee (July 2003): The semantics and execution of a synchronous block-diagram language.
Science of Computer Programming 48, pp. 21–42(22).
[13] J. Eker, J. W. Janneck, E. A. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuendorffer, S. Sachs & Y. Xiong (2003):
Taming Heterogeneity—the Ptolemy Approach. Proceedings of the IEEE 91(2), pp. 127–144.
[14] Sz. Gyapay, D. Varró & R. Heckel (2003): Graph Transformation with Time. Fundam. Inform. 58(1).
[15] E. A. Lee (1999): Modeling concurrent real-time processes using discrete events. Annals of Software Engineering 7(1-4), pp. 25–45.
[16] E. A. Lee & H. Zheng (2007): Leveraging Synchronous Language Principles for Heterogeneous Modeling
and Design of Embedded Systems. In: EMSOFT’07, ACM.
[17] J. Meseguer & P. C. Ölveczky (2009): Formalization and Correctness of the PALS Pattern for Asynchronous
Real-Time Systems. Technical Report, Department of Computer Science, University of Illinois at UrbanaChampaign. http://hdl.handle.net/2142/14214.
[18] P. C. Ölveczky, A. Boronat & J. Meseguer (2010): Formal Semantics and Analysis of Behavioral AADL
Models in Real-Time Maude. In: Proc. FMOODS/FORTE’10, Lecture Notes in Computer Science, Springer.
To appear.
[19] P. C. Ölveczky & J. Meseguer (2002): Specification of real-time and hybrid systems in rewriting logic.
Theoretical Computer Science 285, pp. 359–405.
[20] P. C. Ölveczky & J. Meseguer (2007): Abstraction and Completeness for Real-Time Maude. Electronic Notes
in Theoretical Computer Science 176(4), pp. 5–27.
[21] P. C. Ölveczky & J. Meseguer (2007): Semantics and Pragmatics of Real-Time Maude. Higher-Order and
Symbolic Computation 20(1-2), pp. 161–196.
[22] J. E. Rivera, F. Durán & A. Vallecillo: On the Behavioral Semantics of Real-Time Domain Specific Visual
Languages. In: Proc. WRLA’10, Lecture Notes in Computer Science, Springer. To appear.
[23] SAE AADL Team (2009). AADL Homepage. http://www.aadl.info/.

