Translation from high-level specification languages
Interactive, guided, and exhaustive simulation
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).
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:
"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 (Marius.Bozga@imag.fr) and L. Mounier (Laurent.Mounier@imag.fr)
Binaries and libraries
Documentation (PostScript) and examples
Unix platforms under Linux or Solaris 2.x
SDL and IF specifications (an Object-Geode licence is required for SDL).
IF specifications and automata