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).
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.
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 1: between any two
commands sent by the flight software to the valves there should elapse
at least 50ms.
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]
Home
