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


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


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:

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

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


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

Contact persons : M. Bozga ( and L. Mounier (

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