@inproceedings{BFG+99e,
title = { {IF}: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems },
author = {Bozga, Marius and Fernandez, Jean-Claude and Ghirvu, Lucian and Graf, Susanne and Krimm, Jean-Pierre and Mounier, Laurent},
month = {sep},
year = {1999},
booktitle = {Proceedings of Symposium on Formal Methods 99, Toulouse},
number = {1708},
publisher = {Springer Verlag},
series = {LNCS},
volume = {1708},
team = {DCS,PACSS},
abstract = {We present work of a project for the improvement of a specification/validation toolbox integrating a commercial toolset ObjectGeode and different validation tools such as the verification tool <A HREF=http://www.inrialpes.fr/vasy/cadp.html>CADP</A> and the test sequence generator <A HREF=http://www-verimag.imag.fr/DIST_SYS/TGV/>TGV</A>. The intrinsic complexity of most protocol specifications lead us to study combination of other techniques such as static analysis and abstraction together with the classical model-checking techniques. Experimentation and validation of our results in this context motivated the development of an intermediate representation for SDL called <A HREF=http://www-if.imag.fr>IF</A>. In this intermediate representation, a system is represented as a set of timed automata communicating asynchronously through a set of buffers or by rendez-vous through a set of synchronization gates. The advantage of the use of such a program level intermediate representation is that it is easier to interface with various existing tools, such as static analysis, abstraction and compositional state space generation. Moreover, it allows to define for SDL different, but mathematically sound, notions of time. The purpose of this paper is to show that the intermediate representation IF can serve as a basis for the interconnections of various tools with different input languages into a unified validation framework. },
}
