OMEGA UML profile
This page describes the OMEGA UML profile
defined in project and its semantics; it answers some questions,
choice of UML and the particular profile chosen and about the problems
UML profile. 1
concerning profile and
The choice of the subset of UML that we have
made can be considered as relatively standard with respect to the
commercial UML tools for simulation and/or code generation for
embedded systems, such as Rhapsody, Telelogic TAU and Rose Real-Time,
from ROOM. These tools mainly focus on what is called a “platform
independent” description of the system, that is a model focussing
software structure and on the functionality of an application,
the middleware, OS, hardware architecture,… it is going to be executed
A so-called “platform dependent” model
should provide in addition, enough information to generate code or to
non-functional aspects for a given platform. Notice that the UML profile
Scheduling, Performance and Time (SPT) [SPT03]
– focuses like we do – on the analysis of time
related properties; to this aim, it provides concepts for defining
kinds of “resources”, “task” needing a resource to be executed and
some quantities, in particular time.
An aim of the Omega project is to handle these
two aspects less independently as they are in most existing tools. The
to use less violent abstractions of one aspect when verifying the
cases where this is needed.
The profile has been defined in phases. First,
a so called Kernel Model, has been defined, representing a useful
subset, rich enough, to start the work on the tools and the case
studies. In particular,
the combined modelling synchronous and asynchronous parts of a system,
important issue in some of the case studies. The criteria for the
this profile are the usefulness for the potential users, the
the chosen notations in the CASE tools, the semantic choices of
tools and the possibility to provide rapidly some verification tool
the chosen notations. In a second phase, notations for the expression
constraints, of requirements and for structuring models are defined.
For the OMEGA Kernel Model, we have
chosen, like the considered CASE tools, a relatively complete subset of
operational part of UML, where
- The static structure of the system is described in terms
of a class diagram with only a few restrictions, where associations
between classes express inclusion or accessibility.
- In particular, like the standard profile, we distinguish
between active and passive classes, but with a particular
interpretation: the behaviour of an active class and all the classes
owned or created by it, represent a mono-threaded behaviour, executing
request in a run-to-completion fashion. This notion of activity group
is also used in Rhapsody, and is similar to the notion of process in
SDL or capsule in ROOM.
- Communication between objects is either via asynchronous
signals or via synchronous operation calls, where we distinguish
between primitive operations which are executed by the calling thread
and normal operations which are scheduled by the active object of the
- The behaviour of the system is described by means of an
explicit imperative action language which can be used in combination
with a form of state machine notation for describing transition systems
extended with data, communication and object creation.
Real-time extensions and observers
UML 1.4 includes no support for real-time, but
a profile for Scheduling Performance and Time (called SPT profile) had
defined, including some extensions for the expression of timing
mainly in the form of tag values. We have defined a real-time profile
respects the SPT profile which takes over most of its basic concepts,
concrete syntax where this is missing and specifies the usage. Also,
to the SPT where time constraints are mainly expressed at instance
Omega real-time profile enables time constraints at class level.
- We have introduced the notions of timer and clock,
as they exist in other modelling formalism and as they have been
introduced in UML 2.0. Timers can be set and deactivated and cause a
“timeout event” after a specified duration and clocks can be set and
deactivated, and when active, they count the duration since they have
been set for the last time. This allows the definition of time
dependent behaviour by means of new primitives in the action language.
- We provide syntactic access to semantic level events. A
semantic level event is a state change in the underlying dynamic
semantic. Each syntactic construct may have to 0, 1 or more semantic
level events associated. With a state an enter and an exit
event is associated, with a signal transmission, a send, a receive
and a consume event. A syntax is defined for identifying all
state changes. An event can be defined as a class stereotyped
<<event>> with predefined parameters depending on their
type (all events have an occurrence time, a send-signal event has a
sender, a receiver, a signal type, signal type depending parameters)
and possibly user defined attributes. Moreover, there are means to
refer to different occurrences of an event in a given execution or
prefix of it.
- Expressions of the type duration which can be used in
time constraints can be defined simply using arithmetic expressions on
clocks and the occurrence time attribute of different events (this is
the access to time and duration used in OCL, see below and in
observers, see next item), by a set of predefined duration expressions
- Time constraints may be arbitrary Boolean expressions
depending on time and duration expressions, but we consider only linear
constraints in all our tools. Time constraints can occur
- In the
form of guards in state machines and observers,
time constraints or constraint patterns associated with different UML
construct, as they are foreseen in SPT (WCET associated with methods, minDelay,
maxDelay associated with channels,…) ; notice that such
derived constraints are presently not implemented in the tools, they
have to expressed using the basic means for expression of time
- We have introduced observers mainly as a
means for expressing complex time constraints using a UML operational
syntax, accessible to the user. They are defined as stereotyped of
state machines, where transitions are triggered by semantic level event
occurrences (they can be identified using explicitly defined
event instances or by using an event matching clause as in the
definition of a corresponding event class). An observer allows
expressing constraints on the order and/or timing of occurrence of
semantic level events and is a means to define dynamic properties
depending on time or not. Observers have proven to be well accepted by
users. They express safety properties in the form of acceptors (an
execution leading to an <<error>> state represents an error
trace). In addition, observers can express assumptions (a sequence
leading to an <<invalid>> state is “not to be considered”).
- Finally, some minimal concepts have been introduced to
define scheduling constraints and general scheduling policies.
OCL has been developed as a constraint and
query language for static UML models and does therefore not adequately
the dynamic behaviour of objects and systems. To overcome this
distinguish between local constraints, which are used to specify the
of an object without referring to the context in which it is used, and
constraints, which are used to specify the context in which object
how objects are connected. This distinction is achieved by using the
stereotypes <<local>> and <<global>> which are
to constraints. Additionally, we defined a trace logic in OCL which
an object's behaviour in terms of constraints of traces of events it
observe. The trace logic is a conservative extension of OCL 2.0, where
provide data types for events, very similar to the events presented in
preceding section, and a logical constant “trace” of type Sequence of
which designates the local trace. For global specifications, we
corresponding global assertion language, which is a generalisation of
assertion language. Finally, these assertion languages include
specifying global constraints by providing component and system
is necessary, because OCL 2.0 assumes that the context, in which a
is to be evaluated, is an object and not a collection of objects.
This extension of OCL allows one to capture all
safety properties of an object in a way similar to LSC or sequence
without being bound to refer or provide an objects environment.
In OMEGA, we have anticipated the UML2.0
component model by using the notations provided by the profiles
presently in tools. Components encapsulate their internal description
interact only through a certain kind of objects which are called ports.
are instances of internal classes which are represented by roles. Roles
information about the required and provided operations of these classes
means of interfaces.
Another distinguishing feature of the OMEGA
component model is that ports can dynamically instantiate their
required interfaces which are used to represent external classes
other components. Connectors wire roles of different components
form a component-based application, and a required interface I
acts as placeholder for the external class realizing the role wired to I.
Notice that Components in UML 2.0 do not
encapsulate their internal structure. In OMEGA a component does
internal class structure because in OMEGA we have defined the relation
the internal class structure of a component and its (provided and
interfaces at the level of the action language for state machines. A
characteristic feature of this relation is that the state machines
the behaviour of ports in general contain actions for instantiating
interfaces. By the component connectors these required interfaces are
associated to the classes describing the ports of another component.
Consequently, component connectors in OMEGA allow for the
dynamic creation of ports.
OMEGA components are used to structure sets of
classes and to support a modelling discipline based on interfaces.
Based on the
connections provided by a component system diagram, we formalize the
in terms of the semantics of the underlying class structure. The
defined as the concurrent behaviour of the objects living in the
renaming the required interfaces in the corresponding state-machines by
realizations as specified by the connections.
The CASE tools Rhapsody and Rational Rose do
not support components yet. As a workaround, a component based design
done within the Kernel Model Language by modelling components as
can also associate LSCs and OCL assertions to components to specify the
behaviour of their ports. One can also associate with each role of a
a state machine describing the externally observable behaviour of its
instances. The resulting set of state machines describes the overall
of the ports of a component. The interactions between the ports of
components then can be model-checked by the OMEGA tools.
OMEGA also started preliminary work on a
compositional semantics of components. Such a semantics forms the basis
further development of compositional verification techniques which
separating the verification of the observable interactions between
from the verification of their implementation.
Sequence diagrams are widely used by UML users,
but their UML 1.4 version is not expressive enough, as they can
describe only a
particular (desired or forbidden) execution of a particular set of
to the order of independent events.
For this reason, we have chosen Live Sequence
a formalism extending the existing versions of
Sequence charts (MSC, High Level MSC,…) by adding
- Quantifiers, stating that either there exist an execution
or all executions with a certain prefix are compatible with a given
chart (distinction of existential- or possible - and universal
– or mandatory -charts)
- Liveness constraints by marking certain events
“mandatory” (so called hot conditions) to distinguish which
observations of prefixes are considered to satisfy the chart and which
These Live Sequence charts have been extended
in Omega for taking into account Object Orientation and timing
- The Global time progress supposed in Omega is represented
by an external event tick, representing time progress by one
time unit. LSC specifications can store time in variables and
conditions can contain constraints on such variables, similar as in
timed automata. Due to the distinction between mandatory and non
mandatory conditions, this allows to distinguish between reaction to
external time progress and time dependent requirements.
- The extension to object orientation and dynamic systems
is obtained by allowing the interpretation of “life lines” as classes
(a set of potential instances) and the introduction of quantifiers on
life lines. This allows distinguishing the case where the event
specified by the LSC should be observed in all existing instances of a
class at the instant of occurrence of the corresponding event, and the
case where the behaviour must be observed in at least one such instance.
A set L of events traces and conditions
satisfies a set of LSC charts if each trace in L
all universal charts and for each existential chart there exists at
trace satisfying it. A trace in L satisfies a universal
in its projection on the set A of events and conditions
by the chart is of the form
(A*-prechart)∞ U ((A*-prechart);prechart;mainchart)∞
description of the semantics of LSC can be found in [D1.2.2-b].
The profile is defined by a set of documents
describing a set of admitted constructs and other restrictions, a set
stereotypes and tag values that can be used and their meaning, as well
library containing the definition of time-related data types (available
Rational Rose and in I-Logix Rhapsody formats).
- Operational Kernel model: the kernel model is defined by
some restrictions of the UML 1.4 profile and a few extensions with
stereotypes and predefined tag values. Descriptions can be found in the
All the tools developed in OMEGA are based on the kernel model and
consider at least a subset of it. The document [Syntax]
provides an overview on the accepted syntax, including the Omega Action
Language OMAL which is accepted by the Omega tools.
- Timing extensions: The time extensions consist mainly in
the definition of stereotypes which are described in [GOO04]
and in the syntax document [Syntax].
We have defined a library that contains the definition of time-related
data types. The library is part of the IFx distribution.
- OCL: The OCL extensions are defined as a conservative
extension of OCL2.0, where the extensions are described in [KdB03a,KdB03b,KdB04].
It tries to subsume part of the expression language of the timing
extensions, but uses a different syntax. Its syntax is defined in the
- Component model: The component model is defined mainly in
terms of syntax conventions which are described in the document [Syntax].
- LSC: LSC are a particular form of sequence diagrams,
originally defined in [DH01]
explaining graphical syntax. More recent descriptions with extensions
are defined in [HM02,MHK02,LSCuser04,D1.2.2-b].
Graphical editors are implemented in Weizmann’s PlayEngine and in
OFFIS’ UVE tool.
We have defined a formal semantics for all
parts of the system in terms of sequences of the above defined semantic
where time extensions add an occurrence time to events. The problem
the tools, is answering a question of the form
assumption + mode l |= property ?
where environment, model and property
may be expressed using different formalisms, but for each one a single
used. The question can be reduced to a question of the form
L(environment assumption + model)
\subseteq L(property) ?
and this is
well defined if the (timed and untimed) semantics of the formalisms
models and properties are defined independently. Ensuring consistency
as usual, the problem of the tool builder to correctly implement an
solving this question.
Notice that one of the aims of OMEGA was to
provide a new profile for Real-time and embedded systems which extends
expressivity of the currently existing tools. For this reason, today,
can not use the analysis tools together with the code generator of his
tool as none of them generates code in accordance with the Omega
The questions about semantic choices were
discussed mainly for the operational Kernel model and for the time
One motivation of the project was the
definition of a profile and semantic framework appropriate for the
of mixed synchronous/asynchronous systems. In this context arose the
on how to handle the non determinism induced by concurrency and if and
restrict non determinism of time progress.
- Synchronous approaches impose often deterministic time
progress (in fact maximal system progress) whereas asynchronous models
in general assume external time (non controllable time progress). Timed
automata with urgency allow any kind of control over time progress, but
earlier experience showed that explicit transition urgencies are not
accepted by users. For time extended operational specification, this
lead us to the proposal of some choices of urgency modes handling this
issue implicitly, and it turned out that this was sufficient for the
considered case studies. In LSC, one of these options is chosen, and
time progress is determined by the environment, where the environment
is only taken into account in stable states and only one environment
event is available at a time. In OCL, this is somehow a non issue as it
is used only in a declarative manner. When working only with OCL
without the existence of a operational model, which is what we have
mainly done, restrictions on non determinism and time progress can be
imposed by a set of axioms.
- As a result, using the Kernel model with the notion of
activity group (extended with time), we can accommodate so-called GALS
(Globally asynchronous, locally synchronous Systems). Nevertheless,
this needs still some undesired workaround for those users used to the
use of synchronous languages, such as Esterel, Lustre or Signal.
- We have looked into the interest of general coordination
frameworks, and we have developed a component model based on a very
general notion of interaction between a possibly variable number of
components based on lattices of interactions complete interactions. We
have showed that this framework allows a more direct integration of
synchronous and asynchronous systems [GS02,GS03,GS04].
Nevertheless, it was not possible to integrate this work directly into
our UML profile as it would have required in addition a different type
of diagrams not accessible through existing UML tools.
The work on semantics generated several
unexpected problems and lead to some reflections on how to deal with
have obtained some insights, but there are still many open questions:
It turned out that the
initially provided version of the semantics, that everybody believed to
understand in a first approximation, led to many misinterpretations and
endless discussions amongst the partners. This motivated on one hand,
elaboration of several abstract semantics on more restricted subsets of
profile. It motivated also the work on the semantic exploration tool
some more long term reflections on how to represent semantic choices in
to understand way.
An implementation of
the chosen semantics, such as they are provided by the RML and the IFx
together with a well chosen set of examples are probably a good way to
demonstrate by examples the user what the semantics of a tool is, but
not be the only information given to the user – just like use cases, it
never be complete.
The usage of explicit
priority rules makes semantic variations easily recognizable if these
variations correspond to a particular elimination of non determinism.
Abstract semantics (of
small sub-calculi) can also be helpful in this respect, but there
rather to provide insight about the essentials of the considered
calculus or to
help understanding the consequences of the choice between to options
given variation point. In particular, we have developed an abstract
The previous problem
motivated us to try to identify all potential semantic variation
points. It was
already clear from the experience with state chart semantics that the
variation points is very high in presence of parallel and deep history
and therefore we left these features aside in a first approach. A study
provided in deliverable [D.1.1.4]
shows that the possible variation points concerning
method invocation is also very high; moreover, the number of variation
increases considerably with the granularity. This shows that it is
practicable to provide the user an explicit choice for all variation
As one of the
objectives of the project was to enable a compositional approach to
verification, some effort was spent to provide a compositional
instead of the initial global semantics. The difficulty to provide such
semantics comes from the aim to design a semantics which is both
and abstract; this provides information on the minimal information
the verification of a set of relevant properties, and indeed, we
interesting results here.
In OMEGA, a formal theory has been
developed for reasoning compositionally about the behaviour of a system
terms of its class invariants. A class invariant describes in a generic
the local communication traces of the instances of a class. The
the system is given as a set of global communication traces. In
communication traces formalize message sequence charts in UML and
the actual creation of objects.
The compositional proof theory
provides an axiomatic characterisation of unbounded class instantiation
level of abstraction provided by the communication traces.
verification techniques based on communication traces have been applied
successfully to the MARS example.
Erika Ábrahám, Marcello M. Bonsangue, Frank S. de
Boer, Martin Steffen Object
Connectivity and Full Abstraction for a Concurrent Calculus of Classes
In To appear in the LNCS Proceedings of the First International
on Theoretical Aspects of Computing, ICTAC 2004
Harald Fecher, Marcel Kyas, Frank de Boer, Variation
Points of the Semantics concerning Methods, December 2003
D. Harel, H. Kugler, R. Marelly, A. Votintseva, J. Klose, B. Westphal,
D1.2.2-b, Live Sequence charts for UML and their semantics
Werner Damm, Bernhard Josko, Amir Pnueli, Angelika Votintseva Understanding
UML: A Formal Semantics of Concurrency and Communication in Real-Time
In Frank de Boer, Marcello Bonsangue, Susanne Graf, Willem-Paul de
(Eds.) Proceedings of the 1st Symposium on Formal Methods for
Objects (FMCO 2002) LNCS Tutorials vol. 2852 2003
Werner Damm, Bernhard Josko, Amir Pnueli, Angelika Votintseva A
discrete-time UML semantics for concurrency and communication in
safety-critical applications In Science of Computer
W. Damm and D. Harel. LSCs: Breathing Life into
Sequence Charts. Formal Methods in System Design, 19(1):45 -- 80,
Susanne Graf, Ileana Ober, Iulian Ober Timed
annotations in UML accepted to STTT, Int. Journal on
Tools for Technology Transfer Springer Verl. 2004
Joseph Sifakis. Scheduler
Modelling Based on the Controller Synthesis Paradigm In Journal
of Real-Time Systems, special issue on Control Approaches to Real-Time
Computing vol. 23 2002
Gregor Gössler, Joseph Sifakis Composition
for Component-Based Modeling In 1st Symposium on Formal
for Components and Objects, revised lectures LNCS Tutorials vol.
Gregor Gössler, Joseph Sifakis Priority
systems In proceedings of FMCO'03 LNCS 3188 2004
Susanne Graf, Andreas Prinz Time
- Some problems and solutions In ASM 2005, to appear in
D. Harel, R. Marelly Playing
Time: On the Specification and Execution of Time-Enriched LSC
10th IEEE/ACM Int. Symp. on Modelling, Analysis and Simulation of
Telecommunication Systems (MASCOTS 2002), Fort Worth, Texas 2002
R. Marelly, D. Harel, H. Kugler Multiple
Instances and Symbolic Variables in Executable Sequence Charts
17th Ann. ACM Conf. on Object-Oriented Programming, Systems, Languages
Applications (OOPSLA'02) 2002
D. Harel and R. Marelly, "Play-Engine User's Guide" Play-Book
Marcel Kyas, Frank de Boer, Assertion
Languages for Object
UML, Omega Deliverable D1.2.1, 9. January 2003
Marcel Kyas, Frank de Boer, Addendum
to Assertion Languages for
Structures in UML, Omega Deliverable D1.2.1b, 18. July 2003
Marcel Kyas, Frank de Boer, On
Message Specification in UML, In:
Boer, Frank S. and Bonsangue, Marcello (eds.) Compositional
UML, ENTCS vol. 101, 2004
Marcel Kyas, Joost Jacob, Ileana Ober, Iulian Ober, Angelika
syntax for users, Omega Deliverable D2.2.3 Annex 1. January 2005.
the OMG RFP for Schedulability, Performance and Time, v. 2.0