IF: An intermediate representation and validation environment for timed asynchronous systems

Formal Description Techniques (FDT), such as LOTOS or SDL are at the base of a technology for the specification and the validation of telecommunication systems. Due to the availability of commercial tools, these formalisms are now being widely used in the industrial community. Alternatively, a number of quite efficient verification tools have been developed by the research community. But, most of these tools are based on simple ad hoc formalisms and the gap between them and real FDT restricts their use at industrial scale. This context motivated the development of an intermediate representation called IF which is presented in the paper. IF has a simple syntactic structure, but allows to express in a convenient way most useful concepts needed for the specification of timed asynchronous systems. The benefits of using IF are multiples. First, it is general enough to handle significant subsets of most FDTs, and in particular a translation from SDL to IF is already implemented. Being built upon a mathematically sound model (extended timed automata) it allows to properly evaluate different semantics for FDTs, in particular with respect to time considerations. Finally, IF can serve as a basis for interconnecting various tools into a unified validation framework. Several levels of IF program representations are already available via well defined APIs and allow to connect tools ranging from static analyzers to model-checkers.