The information listed on this page refers to the state of the tool in '99. For more recent information, please use the following link:

http://www-verimag.imag.fr/~async/IF

IF - VERIMAG

Name: IF (Intermediate Format for asynchronous timed systems)

Main Functionalities

Translation from high-level specification languages

Interactive, guided, and exhaustive simulation

Derived Features

Verification of behavioral and logical specifications (model-checking) through connections with CADP (Verimag/Inria Rhone-Alpes) and SPIN (Bell Labs).

Automatic test case generation through a connection with TGV (Verimag/Irisa).

Static Analysis

Description

The intrinsic complexity of most protocol specifications lead us to study combination of classic model-checking techniques with other techniques such as static analysis and abstraction.  We have a long experience in construction of validation tools in the domain of distributed systems through the development of the verification tool CADP (together with INRIA Rhone-Alpes) and the test sequence generator TGV (together with IRISA). The need to adapt these environments for SDL, motivated the development of an intermediate representation, called IF.  In this intermediate representation a system is modeled as a set of timed automata communicating either asynchronously through a set of buffers or by rendez-vous through a set of synchronization gates. The use of such an intermediate representation confers many advantages:

• IF can be considered as a common representation model for other existing languages such as Promela or for a combination of languages adopting different description styles. Its main aim is to serve as a common format for a "loose"  interconnection of different validation environments.
• IF allows to implement and evaluate different semantics of time for SDL as the underlying model is general enough to encompass a large variety of notions of urgency, time non-determinism and different kinds of real-time constructs.
• IF is a structured, language level format which has a relatively simple syntax (compared to SDL for example) and which provides also several API's and libraries for its use in a validation tool.
• IF allows a flattened description of the corresponding SDL specification with the possibility of direct manipulation, simplification and generally application of analysis algorithms which are not easy to perform using commercial tools which, in general, are closed.

The IF toolset contains already several closely interconnected components, and many others are under development:

• SDL2IF is a translator of SDL specifications into the intermediate representation IF; it relies on an API of ObjectGEODE (CS-Verilog).
• IF.OPEN is a set of modules for the exhaustive simulation and model-checking of IF specifications.
• LIVE is a static analysis tool performing live variable optimization on IF specifications.

Related papers

"The Intermediate Representation IF"
M. Bozga, S. Graf, L.Ghirvu, L. Mounier, J. Sifakis
Verimag Technical Report - 1998

"IF: an intermediate representation for SDL and its applications"
M. Bozga, J.C. Fernandez, S. Graf, L.Ghirvu, L. Mounier, J.P. Krimm, J. Sifakis
Proceedings of SDL'Forum 99 - Montreal

"IF: an intermediate representation and validation environment for timed asynchronous systems"
M. Bozga, J.C. Fernandez, S. Graf, L.Ghirvu, L. Mounier, J.P. Krimm
Proceedings of FM'99 - Toulouse

"State space reduction based on live variable analysis"
M. Bozga, J.C. Fernandez, L.Ghirvu
Proceedings of SAS 99 - Venezia
 

Availability

The IF toolsel is freely distributed to academic institutions for non-profit use.
It can be downloaded from the following URL:

http://www-verimag.imag.fr/DIST_SYS/IF/

Contact persons : M. Bozga (Marius.Bozga@imag.fr) and L. Mounier (Laurent.Mounier@imag.fr)

Format of the distribution

Binaries and libraries

Documentation (PostScript) and examples

Supported platforms

Unix platforms under Linux or Solaris 2.x

Input format

SDL and IF specifications (an Object-Geode licence is required for SDL).

Output format

IF specifications and automata