IST-2001-33522 OMEGA

Correct Development of Real-Time Embedded Systems

Timed system verification : IFx (VERIMAG)

The OMEGA toolset
     Timed system verification
     Untimed system verification
     PVS tools
     LSC tools
The OMEGA UML profile
Case studies
Publications and bibliography
Download documents
Partners & Persons
Related links


Tool description
An example


Tool description

IFx is an extended version of the IF toolbox, developped in the OMEGA project.

IFx works on timed UML models written in the OMEGA profile with widely used commercial CASE tools like Rational Rose or I-Logix Rhapsody. The main functionality provided by IFx is :

  • Simulation : step by step execution, inspection of the system state, conditional breakpoints, scenario rewind/replay, manual resolution of non-determinism, control of scheduling policy and time related parameters, etc.
  • Verification of simple consistency conditions like deadlocks, timelocks, satisfaction of state invariants.
  • Verification of dynamic and timing properties using the model-checkers provided by the IF tool. The properties may be expressed within the choosen UML case tool by means of the following notations provided by the Omega UML profile:
    • observer classes : classes with special state machines reacting to events and conditions occurring in the system execution
    • timing constraints : constraints on durations between system events
    Furthermore, all the property expression formalisms of the tools connected with IF can be used, in particular µ-calculus formulas, but they require knowledge about the entities generated by the translation of UML to IF.
  • The tool can also be used to compare models modulo different simulation and bisimulation relations.

Verification is performed on-the-fly in the IFx environment and allows the generation of diagnostic traces which can be inspected using the simulator.

The architecture of the IFx toolset is depicted below. The upper part shows the UML tools specific to IFx, while the lower part shows the components of the IF toolset, including some modules developed in the OMEGA project (in blue).

IFx tool architecture

The main components of IFx, in addition to the IF tools, are:

  • the UML-to-IF translator whihc takes as input a UML model stored in XMI format. The model may use standard UML constructs and extensions defined by the Omega profile: actions written in the Omega action language, timing annotations and observers expressing model properties. [more infomation on the profile]
       The translator generates an IF specification corresponding to the UML model, according to the Omega semantics. The principles of the translation are described in this paper.
  • the UML front-end provides an interface specifically targeted at UML modelers for the IF validation tools. The interface hides IF and the details of translation and presents simulation and verification results in the vocabulary of the initial UML model. The interface supports all compilation and simulation features mentioned before, and offers customizable views on the analyzed system.

Validation examples

Ariane-5 flight software

The IFx tool has been used to validate the UML model constructed by retro-engineering of an extract of the Ariane-5 flight software, a case study provided by EADS in the scope of the Omega project.

architecture of the Ariane-5 model

The architecture of this case study is shown in the figure above. Components drawn in blue represent the environment of the software: the equipment that is controlled, or the actors that interact with it from the ground. Components drawn in yellow are the modules of the flight software:

  • Mission management modules (Regulation) manage the launcher configuration and the mission phases. They control events like igniting an engine, releasing a stage, etc.
  • Guidance, navigation and control modules (GNC) perform the flight control of the launcher: navigation, guidance, control, thrust monitor, etc.
IFx has been used in this case study :
  • to statically validate the model by syntax cheching, type checking, simple static analysis (e.g., dead code detection)
  • to prove 9 timed safety properties of the flight regulation modules,
  • to analyze the schedulability of the regulation and the GNC components under the assumption of a fixed priority preemptive scheduling policy. Scheduling objectives were expressed as observers and verified against the model. An example of objective is that the GNC code, which is executed cyclically, meets its deadline each time.

Below are some of the properties which were verified with IFx on the Ariane-5 model. They are expressed as observers.

Property : between any two commands sent by the flight software to the valves there should elapse at least 50ms

Property 1: between any two commands sent by the flight software to the valves there should elapse at least 50ms.

property 2

Property 2: if some instance of class Valve fails to open (i.e. enters the state Failed_Open) then:

  • No instance of the Pyro class reaches the state Ignition_done
  • All instances of class Valve shall reach one of the states Failed_Close or Close after at most 2 seconds since the initial valve failure.
  • The events EAP_Preparation and EAP_Release are never emitted.

Other examples

IFx has also been used for the verification of timed safety properties in two other Omega case studies : MARS (Medium Altitude Reconnaissance System) by NLR and a Sensor Voting and Monitoring system by IAI. Details are available here.

Resources and downloads

Download the tools at this page for one of the following platforms:

  • Linux iX86
  • Solaris
  • Windows  - Cygwin (for GNU GCC users)
  • Window - native (for Visual C++ users)

The following documents describe different aspects of the toolset:

  • A paper presenting the tool principles and the Ariane-5 case study :
    Iulian Ober, Susanne Graf, Ileana Ober Validating timed UML models by simulation and verification. Accepted for publication in STTT, Int. Journal on Software Tools for Technology Transfer. Springer Verlag, 2004. [download]
  • A paper presenting the real-time features of the Omega profile :
    Susanne Graf, Ileana Ober, Iulian Ober. A real-time profile for UML. Submitted to STTT, Int. Journal on Software Tools for Technology Transfer Springer Verlag 2004 [download]
  • Slides of an IF tutorial (given at SPIN'2004) [download]
  • A deliverable on the syntax of different model elements (actions, observers, timing constraints) [download]

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