| 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
slides |
| 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
slides
|
| 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
slides |
|
|
| 13:40 - 14:15
|
Semantic Considerations in Omega.
Frank de Boer - CWI, Bernhard Josko - OFFIS
slides |
| 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
slides |
| 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 http://www-verimag.imag.fr/~ober/IFx/
|
| 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.
slides |
| 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
slides |
|
|
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.
slides |
|
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
slides |
|
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.
|
Home