Paper Info
Title
IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems
Abstract
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.
Year
DOI
Venue
1999
10.1007/3-540-48119-2_19
World Congress on Formal Methods
Keywords
Field
DocType
real fdt,validation environment,asynchronous system,industrial community,simple syntactic structure,unified validation framework,intermediate representation,timed asynchronous systems,research community,different semantics,formal description techniques,industrial scale,commercial tool,model checking,static analysis
Asynchronous communication,Model checking,Programming language,Computer science,Concurrency,Static analysis,Real-time computing,Formal specification,Systems architecture,Rotation formalisms in three dimensions,Distributed computing,Formal verification
Conference
Volume
ISSN
ISBN
1708
0302-9743
3-540-66587-0
Citations 
PageRank 
References 
43
2.29
30
Authors
6
Name
Order
Citations
PageRank
Marius Bozga12100127.83
Jean-Claude Fernandez239529.17
Lucian Ghirvu320212.69
Susanne Graf440024.11
Jean-pierre Krimm516310.57
Laurent Mounier6118779.54