IF Toolset

 Features

Language

• structuring concepts: systems consist of processes, running in parallel and communicating through message passing via communication buffers
• communication primitives: processes may communicate either through signal exchange (directly or via signalroutes) or through shared variables
• real-time primitives: each process may use several clocks to measure time during the execution and, in addition, transitions may be guarded with time constraints (depending on clocks) and decorated with explicit (eager, delayable, lazy) deadlines
• open systems: the language offers the concept of open communication channel, connected to the environment, and transporting messages between it and the system
• non-determinism: processes may be non-deterministic i.e, more than one transition may be enabled at some control state, and all situations have to be considered at execution
• complex data types: the language provide several type constructors such as enumeration, range, array, record, abstract as well as predefined basic types in order to simplify complex data description and manipulation
• parameterisation: it is now possible to parameterize data types (i.e, size of arrays), system configurations (i.e, number of instances), timing behavior (i.e, clock constraints)...
• dynamic creation: the language include dynamic creation and destruction of process and signalroute (channel) instances. This makes system configuration to be dynamic, that is, the number of components running (and in turn, the number of clocks ...) may change during execution
• structured control: the common language integrates hierachical states (to structure automata) and composed transitions basic control statements such as if-then-else and while-do are provided to structure automata transitions
• external code integration: the common language provide a simple an elegant way to abstract complex transformations on data through the integration of external code within procedures. The external code to be provided depend on tools used i.e, an executable implementation in order to simulate and model check, or a first-order axiomatic definition in order to use it inside a prover, etc.

Tools

• static analysis: IF provides the dfa tool which implements classical static analysis techniques such as live variable analysis, dead-code elimination and variable elimination (backward slicing) with respect to user-defined criteria.
• model-checking: The core component of the IF toolbox is the IF simulator allowing to explore the underlying semantic model (i.e, state graph) of an IF specification. Several exploration modes are imlemented: interactive (user-driven), random or exhaustive (breadth-first or depth-first). Partial order reductions can be applied in exhaustive- depth first search.
• test generation: The IF simulator has been connected to the TGV test generator in the context of the AGEDIS project. See the AGEDIS web page for more details.

Libraries

• model: This library gives access to the abstract syntax tree (AST) of IF specifications. It can be used to implement tools operating "statically" on the specification such as translators to other languages, static analysis and optimisations at source level.
• simulator: A simulation library providing the minimal functionality for on-the-fly state-space traversal (state representation + successors computation) is provided. It can be used to implement tools operating "dynamically" on the specifcation such as exploration tools, model-checkers, simulators, etc.

 IFx/Omega Extension

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 behavioral properties by model checking. The properties may be expressed as :
  • observer objects (accepting state machines reacting to system events and conditions)
  • timing constraints (durations between system events)
  • µ-calculus formulas
• The tool is also connected with other tools, such as labelled transition system manipulation tools from the CADP suite (Aldebaran).

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 which 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 beeen used to validate the UML model of the Ariane-5 flight software, a case study provided by EADS in the Omega project.

The architecture of the Ariane-5 model is shown in the figure below. 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:

• Regulation modules which coordinate the behavior of the launcher as a whole and the behavior of each stage. They control events like firing a stage, releasing a component, etc.
• Guidance, Navigation and Control modules perform the fine-grained control of the launcher’s flight parameters: monitor thrust and other parameters, calculate aiming, 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 cycle, which repeats every 72ms during the flight, finishes 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 here 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

 Download

Licence

/*
 *
 * IF-Toolset - Copyright (C) UGA - CNRS - G-INP
 *
 * by  Marius  -  Iulian  -  Susanne  -  Laurent  -   Joseph
 *       Bozga  -    Ober  -     Graf  -  Mounier  -   Sifakis
 * 
 * This  software is  a computer  program whose  purpose is  to simulate,
 * explore and model-check  real-time systems represented using  the IF -
 * intermediate  format  -  language.   This  software  package  contains
 * sources,  documentation,  and  examples.
 * 
 * This software is governed by the CeCILL-B license under French law and
 * abiding by the  rules of distribution of free software.   You can use,
 * modify  and/ or  redistribute  the  software under  the  terms of  the
 * CeCILL-B license as circulated by CEA, CNRS and INRIA at the following
 * URL "http://www.cecill.info".
 *
 * As a counterpart to the access to  the source code and rights to copy,
 * modify and  redistribute granted  by the  license, users  are provided
 * only with a limited warranty and  the software's author, the holder of
 * the economic  rights, and the  successive licensors have  only limited
 * liability.
 *
 * In this respect, the user's attention is drawn to the risks associated
 * with loading,  using, modifying  and/or developing or  reproducing the
 * software by the user in light of its specific status of free software, 
 * that may  mean that  it is  complicated to  manipulate, and  that also
 * therefore means  that it  is reserved  for developers  and experienced
 * professionals having in-depth computer  knowledge. Users are therefore
 * encouraged  to load  and test  the software's  suitability as  regards
 * their  requirements  in  conditions  enabling the  security  of  their
 * systems and/or  data to  be ensured  and, more  generally, to  use and
 * operate it in the same conditions as regards security.
 * 
 * The fact that  you are presently reading this means  that you have had
 * knowledge of the CeCILL-B license and that you accept its terms.
 *
 */

Requirements

The IF Toolset is available for UNIX-like platforms.

Prerequisites:
Standard C++ development tools: gcc, make, flex, bison, m4
Apache Xerces C++ XML Parser: libxerces-c-dev

Download

Check out from IF Toolset Git Project.

 Documentation

Papers

General

• Tools and Applications II: The IF Toolset. Marius Bozga, Susanne Graf, Ileana Ober, Iulian Ober and Joseph Sifakis. In Flavio Corradinni and Marco Bernanrdo, editors, Proceedings of SFM’04 (Bertinoro, Italy), September, 2004 LNCS vol. 3185, Springer-Verlag [postscript, slides]
• IF-2.0: A validation environment for Component-Based Real-Time Systems. Marius Bozga, Susanne Graf and Laurent Mounier. In Ed Brinksma, K.G. Larsen, editors, Proceedings of CAV’02 (Copenhagen, Denmark), July, 2002 LNCS vol. 2404, Springer-Verlag [postscript, slides]
• Automated validation of distributed software using the IF environment. Marius Bozga, Susanne Graf, and Laurent Mounier. In Scott D. Stoller and Willem Visser, editors, Workshop on Software Model-Checking, associated with CAV’01 (Paris, France) July 2001 Volume 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers. [postscript, slides]
• IF: A Validation Environment for Timed Asynchronous Systems. M. Bozga, J.Cl. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier. Proceedings of CAV’00 (Chicago, USA) July 2000 [postscript, slides]
• IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. M. Bozga, J.Cl. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier. Proceedings of FM’99 (Toulouse, France) September 1999. [postscript, slides]

Real-Time SDL and UML

• Model-checking UML models via a mapping to communicating extended timed automata. Susanne Graf, Ileana Ober and Iulian Ober. In Susanne Graf and Laurent Mounier, editors, Proceedings of SPIN’04 (Barcelona, Spain), April, 2004. [pdf, slides]
• Timed Extensions for SDL. M. Bozga, S. Graf, L. Mounier, I. Ober, J-L. Roux, D. Vincent. Proceedings of SDL-Forum’01 (Copenhagen, Denmark) June 2001. [postscript, slides]
• SDL for Real Time: What is Missing? M.Bozga, S.Graf, A. Kerbrat, L. Mounier, I. Ober, D. Vincent. Proceedings of SAM’00 (Grenoble, France) June 2000. [postscript, slides]
• IF: An Intermediate Representation for SDL and its Applications. M. Bozga, J.Cl. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier, J. Sifakis. Proceedings of SDL-Forum’99 (Montreal, Canada) June 1999. [postscript, slides]

Verification and Testing

• Testing conformance of real-time software by auto;atic generation of observers. Saddek Bensalem, Marius Bozga, Moez Krichen and Stavros Tripakis. In Proceedings of RV’04 (Barcelona, Spain), April, 2004 [postscript, slides]
• Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems. J.P. Krimm, L. Mounier. Proceedings of TACAS’00 (Berlin Germany) April 2000. [postscript, slides]

Static Analysis

• Using Static Analysis to Improve Automatic Test Generation. M. Bozga, J.Cl. Fernandez, L. Ghirvu. Proceedings of TACAS’00 (Berlin, Germany) April 2000. [postscript, slides].
• State Space Reduction based on Live Variable Analysis. M. Bozga, J.Cl. Fernandez, L. Ghirvu. Proceedings of SAS’99 (Venetia, Italy) September 1999. [postscript, slides]

Case Studies

• Experiment on Verification of a Planetary Rover Controller. Anahita Akhavan, Saddek BEnsalem, Marius Bozga and Eleni Orfanidou. In Proceedigs of IWPSS’04 (Darmstadt, Germany), June, 2004. [pdf, slides]

• Model-Checking Ariane-5 Flight Program. M. Bozga, D. Lesens, and L. Mounier. In Proceedings of FMICS’01 (Paris, France), pages 211-227. INRIA, 2001. [postscript, slides]
• Verification experiments on the MASCARA protocol. Susanne Graf and Guoping Jia. In Proceedings of SPIN Workshop ’01 (Toronto, Canada) January 2001. [postscript, slides]

Tutorials

A brief introduction to observers

and their semantics

 Links

Projects

RNRT PROUST
Esprit LTR VIRES
IST INTERVAL
IST ADVANCE
IST AGEDIS
IST OMEGA
Full MDE

Languages

Specification and Description Language
Unified Modelling Language

Tools

PragmaDev
Rhapsody
ObjectGEODE
CADP
SPIN
Kronos
Uppaal
TReX
Verisoft
SystemC

Contributors

Marius BOZGA
Susanne GRAF
Iulian OBER
Laurent MOUNIER
Joseph SIFAKIS