IST-2001-33522 OMEGA

This page describes the OMEGA UML profile defined in project and its semantics; it answers some questions, concerning the choice of UML and the particular profile chosen and about the problems concerning semantics.

UML profile. 1

• Operational profile and Kernel Model 1
• Real-time extensions and observers. 2
• OCL 3
• Component model 3
• Live Sequence Charts. 4
• Availability of the profile. 5

• Consistency of semantics. 5
• Semantic choices. 6

References concerning profile and semantics. 7

UML profile

The choice of the subset of UML that we have made can be considered as relatively standard with respect to the choices of commercial UML tools for simulation and/or code generation for real-time and embedded systems, such as Rhapsody, Telelogic TAU and Rose Real-Time, emerging from ROOM. These tools mainly focus on what is called a “platform independent” description of the system, that is a model focussing on the software structure and on the functionality of an application, independently of the middleware, OS, hardware architecture,… it is going to be executed on.

A so-called “platform dependent” model should provide in addition, enough information to generate code or to analyze non-functional aspects for a given platform. Notice that the UML profile for 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 different kinds of “resources”, “task” needing a resource to be executed and consuming 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 aim is to use less violent abstractions of one aspect when verifying the other, in cases where this is needed.

The profile has been defined in phases. First, a so called Kernel Model, has been defined, representing a useful operational 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, is an important issue in some of the case studies. The criteria for the choice of this profile are the usefulness for the potential users, the availability of the chosen notations in the CASE tools, the semantic choices of existing UML tools and the possibility to provide rapidly some verification tool support for the chosen notations. In a second phase, notations for the expression of time constraints, of requirements and for structuring models are defined.

Operational profile and Kernel Model

For the OMEGA Kernel Model, we have chosen, like the considered CASE tools, a relatively complete subset of the 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 activity group.
• 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 been defined, including some extensions for the expression of timing properties, mainly in the form of tag values. We have defined a real-time profile that respects the SPT profile which takes over most of its basic concepts, defines a concrete syntax where this is missing and specifies the usage. Also, contrary to the SPT where time constraints are mainly expressed at instance level, the 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,
• conditions in LSC,
• OCL constraints
• explicit 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 constraints
• 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

OCL has been developed as a constraint and query language for static UML models and does therefore not adequately capture the dynamic behaviour of objects and systems. To overcome this short-coming, we distinguish between local constraints, which are used to specify the behaviour of an object without referring to the context in which it is used, and global constraints, which are used to specify the context in which object occur and how objects are connected. This distinction is achieved by using the additional stereotypes <<local>> and <<global>> which are attached to constraints. Additionally, we defined a trace logic in OCL which specifies an object's behaviour in terms of constraints of traces of events it can observe. The trace logic is a conservative extension of OCL 2.0, where we provide data types for events, very similar to the events presented in the preceding section, and a logical constant “trace” of type Sequence of Events which designates the local trace. For global specifications, we introduced a corresponding global assertion language, which is a generalisation of the local assertion language. Finally, these assertion languages include mechanisms for specifying global constraints by providing component and system contexts. This is necessary, because OCL 2.0 assumes that the context, in which a constraint 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 diagrams, without being bound to refer or provide an objects environment.

Component model

In OMEGA, we have anticipated the UML2.0 component model by using the notations provided by the profiles available presently in tools. Components encapsulate their internal description and interact only through a certain kind of objects which are called ports. Ports are instances of internal classes which are represented by roles. Roles export information about the required and provided operations of these classes by means of interfaces.

Another distinguishing feature of the OMEGA component model is that ports can dynamically instantiate their associated required interfaces which are used to represent external classes belonging to other components. Connectors wire roles of different components together to 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 encapsulate its internal class structure because in OMEGA we have defined the relation between the internal class structure of a component and its (provided and required) interfaces at the level of the action language for state machines. A characteristic feature of this relation is that the state machines describing the behaviour of ports in general contain actions for instantiating required 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 inter-component 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 semantics in terms of the semantics of the underlying class structure. The behaviour is defined as the concurrent behaviour of the objects living in the component and renaming the required interfaces in the corresponding state-machines by their 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 can be done within the Kernel Model Language by modelling components as classes. One can also associate LSCs and OCL assertions to components to specify the overall behaviour of their ports. One can also associate with each role of a component a state machine describing the externally observable behaviour of its instances. The resulting set of state machines describes the overall behaviour of the ports of a component. The interactions between the ports of different 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 for the further development of compositional verification techniques which allow separating the verification of the observable interactions between components from the verification of their implementation.

Live Sequence Charts

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 instances up to the order of independent events.

For this reason, we have chosen Live Sequence Charts [DH01], 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 ones not.

These Live Sequence charts have been extended in Omega for taking into account Object Orientation and timing constraints:

• 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 satisfies all universal charts and for each existential chart there exists at least one trace satisfying it. A trace in L satisfies a universal chart, if in its projection on the set A of events and conditions observed by the chart is of the form

(A*-prechart)∞ U ((A*-prechart);prechart;mainchart)∞

A detailed description of the semantics of LSC can be found in [D1.2.2-b].

Availability of the profile

The profile is defined by a set of documents describing a set of admitted constructs and other restrictions, a set of stereotypes and tag values that can be used and their meaning, as well as a library containing the definition of time-related data types (available in Rational Rose and in I-Logix Rhapsody formats).

1. 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 publications [DJP*02,DJP*05]. 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.
2. 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.
3. 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 document [Syntax].
4. Component model: The component model is defined mainly in terms of syntax conventions which are described in the document [Syntax].
5. 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.

Semantics

Consistency of semantics

We have defined a formal semantics for all parts of the system in terms of sequences of the above defined semantic level events, where time extensions add an occurrence time to events. The problem solved by the tools, is answering a question of the form

environment assumption + mode l |=  property ?

where environment, model and property may be expressed using different formalisms, but for each one a single one is 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 used for models and properties are defined independently. Ensuring consistency is now, as usual, the problem of the tool builder to correctly implement an algorithm solving this question.

Semantic choices

Notice that one of the aims of OMEGA was to provide a new profile for Real-time and embedded systems which extends the expressivity of the currently existing tools. For this reason, today, the user can not use the analysis tools together with the code generator of his CASE tool as none of them generates code in accordance with the Omega profile.

The questions about semantic choices were discussed mainly for the operational Kernel model and for the time extensions.

One motivation of the project was the definition of a profile and semantic framework appropriate for the description of mixed synchronous/asynchronous systems. In this context arose the question on how to handle the non determinism induced by concurrency and if and how to 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[1].
• 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 them. We have obtained some insights, but there are still many open questions:

1.      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 almost endless discussions amongst the partners. This motivated on one hand, the elaboration of several abstract semantics on more restricted subsets of the profile. It motivated also the work on the semantic exploration tool RML and some more long term reflections on how to represent semantic choices in an easy to understand way.

·         An implementation of the chosen semantics, such as they are provided by the RML and the IFx tool 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 this can not be the only information given to the user – just like use cases, it will 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 strength is rather to provide insight about the essentials of the considered calculus or to help understanding the consequences of the choice between to options for a given variation point. In particular, we have developed an abstract class calculus [ABBS04].

2.      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 number of variation points is very high in presence of parallel and deep history states 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 points increases considerably with the granularity. This shows that it is probably not practicable to provide the user an explicit choice for all variation points.

3.      As one of the objectives of the project was to enable a compositional approach to verification, some effort was spent to provide a compositional semantics instead of the initial global semantics. The difficulty to provide such a semantics comes from the aim to design a semantics which is both compositional and abstract; this provides information on the minimal information needed for the verification of a set of relevant properties, and indeed, we obtained some interesting results here.

In OMEGA, a formal theory has been developed for reasoning compositionally about the behaviour of a system in terms of its class invariants. A class invariant describes in a generic manner the local communication traces of the instances of a class. The behaviour of the system is given as a set of global communication traces. In general, communication traces formalize message sequence charts in UML and abstract from the actual creation of objects.

The compositional proof theory provides an axiomatic characterisation of unbounded class instantiation at the level of abstraction provided by the communication traces. Compositional verification techniques based on communication traces have been applied successfully to the MARS example.

References concerning profile and semantics

[ABBS04] 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 Colloquium on Theoretical Aspects of Computing, ICTAC 2004

[D.1.1.4] Harald Fecher, Marcel Kyas, Frank de Boer, Variation Points of the Semantics concerning Methods, December 2003

[D1.2.2-b] D. Harel, H. Kugler, R. Marelly, A. Votintseva, J. Klose, B. Westphal, Deliverable D1.2.2-b, Live Sequence charts for UML and their semantics

[DJP*02] Werner Damm, Bernhard Josko, Amir Pnueli, Angelika Votintseva Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML In Frank de Boer, Marcello Bonsangue, Susanne Graf, Willem-Paul de Roever (Eds.) Proceedings of the 1st Symposium on Formal Methods for Components and Objects (FMCO 2002) LNCS Tutorials vol. 2852 2003

[DJP*05] 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 Programming 2005

[DH01] W. Damm and D. Harel. LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design, 19(1):45 -- 80, July 2001

[GOO04] Susanne Graf, Ileana Ober, Iulian Ober Timed annotations in UML accepted to STTT, Int. Journal on Software Tools for Technology Transfer Springer Verl. 2004

[GS02] 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

[GS03] Gregor Gössler, Joseph Sifakis Composition for Component-Based Modeling In 1st Symposium on Formal Methods for Components and Objects, revised lectures LNCS Tutorials vol. 2852 2003

[GS04] Gregor Gössler, Joseph Sifakis Priority systems In proceedings of FMCO'03 LNCS 3188 2004

[GP05] Susanne Graf, Andreas Prinz Time in ASMs - Some problems and solutions In ASM 2005, to appear in LNCS, 2005

[HM02] D. Harel, R. Marelly Playing with Time: On the Specification and Execution of Time-Enriched LSC In Proc. 10th IEEE/ACM Int. Symp. on Modelling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 2002), Fort Worth, Texas 2002

[MHK02] R. Marelly, D. Harel, H. Kugler Multiple Instances and Symbolic Variables in Executable Sequence Charts In Proc. 17th Ann. ACM Conf. on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'02) 2002

[LSCuser04] D. Harel and R. Marelly, "Play-Engine User's Guide"  Play-Book

[KdB03a] Marcel Kyas, Frank de Boer, Assertion Languages for Object Structures in UML, Omega Deliverable D1.2.1, 9. January 2003

[KdB03b] Marcel Kyas, Frank de Boer, Addendum to Assertion Languages for Object Structures in UML, Omega Deliverable D1.2.1b, 18. July 2003

[KdB04] Marcel Kyas, Frank de Boer, On Message Specification in UML, In: de Boer, Frank S. and Bonsangue, Marcello (eds.) Compositional Verification in UML, ENTCS vol. 101, 2004

[Syntax] Marcel Kyas, Joost Jacob, Ileana Ober, Iulian Ober, Angelika Votintseva, OMEGA syntax for users, Omega Deliverable D2.2.3 Annex 1. January 2005.

External References

[SPT03] OMG, Response to the OMG RFP for Schedulability, Performance and Time, v. 2.0 March 2002

[1] Such as those proposed in [GP05] in the context of abstract state machines