IST-2001-33522 OMEGA

Correct Development of Real-Time Embedded Systems

The OMEGA Workshop

The OMEGA toolset
The OMEGA UML profile
Case studies
Publications and bibliography
Download documents
Partners & Persons
Related links

Omega workshop - Programme with abstracts

Omega workshop - Programme with abstracts

09:15 - 09:30 Welcome and Introduction
Morning session: invited talks (09:30-12:15)
09:30 - 10:15 The Fractal component model - Foundations, Pragmatics and Calculus Jean-Bernard Stefani, INRIA Grenoble
Distributed systems programming is moving towards component-based models, including for the construction of middleware layers themselves. The talk will present an example reflective component-model called Fractal, which has been used in the construction of asynchronous middleware and communication subsystems, and the abstract co-algebraic model that underpins it. It will then discuss the formalization of the Fractal operational semantics via an interpretation of the Fractal constructs in the Kell calculus, a higher-order process calculus with localities.
10:15 - 10:45 -- COFFEE --
10:45 - 11:30 UML2.0 with the focus on components Birger Møller-Pedersen, University of Oslo
The talk will present UML2.0, with emphasis on the component model, and show how these and other new developments in UML2.0 support what in Europe is called system family modeling and in the US is called product line modeling.
Interestingly enough, the need for this kind of modeling has led to a heated debate on the usefulness of UML/MDA versus domain specific languages (DSLs). The talk will cover this debate and report from an ongoing research project on a quite different way of doing this.
11:30 - 12:15 Model driven engineering. Myths and reality Jacky Estublier, LSR/CNRS Grenoble
Model driven engineering (MDE) is a generalisation of the Model Driven Architecture (MDA) OMG initiative. It promises a revolution in the techniques and methods in Software engineering, and pretends to be the only way out of the software crisis. This talk presents the fundaments of the approach, its current state, its promises and intent to make a brief assessment of its current and future real potential.
Buffet Lunch (12h15-13h30)
Afternoon session: Results from the OMEGA project
13:30 - 13:40 Short overview on the Omega project Susanne Graf - VERIMAG
13:40 - 14:15 Semantic Considerations in Omega. Frank de Boer - CWI, Bernhard Josko - OFFIS
In this presentation we first discuss the UML kernel model developed in the Omega project and its semantics. We focus on the object-oriented features, synchronous and asynchronous communication, concurrency and resolution of non-determinism using activity groups and timing.
We then identify a number of semantic variation points concerning these issues and we discuss how they have been captured in an abstract semantics and its implementation in an extension of XML, the Rule Mark-up Language (RML). We will also show how our approach to semantics in UML compares to other approaches.
14:15 - 15:00 IF simulation and verification tool for UML and IF for components. Marius Bozga, Iulian Ober, Josef Sifakis - VERIMAG
IF is an open validation platform for asynchronous timed systems built upon a specification language based on timed automata extended with discrete data variables, various communication primitives and dynamic process creation. It is expressive enough to express most useful concepts of widely used modeling and programming languages for distributed systems like SDL, UML or Java at a comparable level of abstraction.
We will first present the toolbox architecture and discuss the components, the state space exploration engine, and the validation-related components: the static analyser, the model checker, the test generator.
In the second part, we present the frontend IFx developed for the OMEGA UML profile, allowing to validate a large subset of operational UML specifications using the IF toolset. IFx includes a compiler of UML models to IF and an interactive simulator which allows replaying diagnostic traces in terms of the original UML model.
Finally, we will present some recent developments for extending IF to a more general component framework with n-ary interactions realized by an appropriate scheduling of the actions of the participating components.
More information on IFx can be found via the webpage of the Omega project or
15:00 - 15:30 -- COFFEE --
Omega Tools and Case studies
15:30 - 16:15 Overview on the toolset and the modelling and verification of the Mars case study Yuri Yushtein - Kiel Univ. and Jozef Hooman - Nijmegen Univ.
We briefly present the Omega tool set in the scope of the Medium Altitude Reconnaissance System (MARS) case study provided by the NLR (Dutch National Aerospace Laboratory). First we describe the application of the Omega tools to the original UML model of MARS, leading to an evaluation of the tools in this context. Next we redesign a part of the case study to facilitate compositional verification techniques and to investigate complementary use of tools in order to gain insight into their combined application. We summarize the results of these experiences.
16:15 - 16:45 Ariane 5 flight program timing verification. David Lesens - EADS

The EADS SPACE Transportation case study has been constructed by retro-engineering of an extract of the Ariane-5 flight software and focuses on relevant real time behaviours currently used in space domain. This presentation will show the interest of using two different semantics of time to describe a spacecraft behaviour: an asynchronous view for the mission management (well adapted to OMEGA profile) and a cyclic synchronous view "a la SCADE" for the spacecraft control / command (which requires an adaptation to be modelled with the OMEGA profile).
It will then show how these two aspects of time, as well as the associated assumptions on the software environment and the associated real-time properties have been modelled together in UML with the OMEGA profile. The results of the IF toolbox (simulator and proof tool) experiments on this case study will be presented as a conclusion.
16:45 - 17:15 Animation and formal verification of a component-based service using live sequence charts (LSCs) and the Play-Engine. Pierre Combes - FTR&D and Hillel Kugler - Weizmann Inst.
The FTR&D application in OMEGA is a depannage service, built by assembling a set of embedded and reusable components. We describe the application of a scenario-based approach to the depannage service model, using live sequence charts and the Play-Engine tool. LSCs are used to describe an abstract view of the system components, focusing on the behavioral interfaces, the communication between the components and time-related aspects. The Play-Engine tool allows executing the requirements while animating system behavior (play-out), thus gaining a better understanding of the system behavior and applying formal verification methods for direct execution and property verification (smart play-out). We summarize our experience and results obtained while applying the tool and methods to the depannage system.
17:15 - 17:45 Timing analysis of a voting monitor with 2 CPUs using LSC and IF. Meir Zenou - IAI
In a fly by wire aircraft, the sensors constitute a critical source of data for the control loops which implement the flight control software producing the servo-actuators commands. Another critical resource is the computer itself . For safety purposes, the system supports a triple redundancy of sensors, computers and communication channels.
The IAI case study model concerns typical mechanisms of "voting" and "monitoring" applied to sensors and computers in the flight control software.
Voting is a mechanism by which the values sampled every cycle on the 3 sensors or the servo commands provided by the 3 computers, are compared one to the other in order to detect whenever one of the 3 values differs from the 2 others. In this case disqualify the discrepant source of data is ignored.
Monitoring is an accounting mechanism in which after a given number of successive "ignore" cases, the sensor or the computer id disqualified.
We have applied three of the Omega tools to this case study: Play Engine for scenario based requirement evaluation, the UVE tool for untimed verification for showing the correctness of the voting algorithm and the IFx tool set for establishing reactivity properties.

Susanne Graf
Last modified: Fri Feb 25 08:26:53 MET 2005

You are currently authenticated as omegapublic (level 0)
For comments about this site please contact the webmaster