Paper Info
Title
If: An Intermediate Representation For Sdl And Its Applications
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 CADP and the test sequence generator TGV.The intrinsic complexity of most protocol specifications lead us to study combinations of techniques such as static analysis and abstraction together with classical model-checking techniques. Experimentation and validation of our results in this context motivated the development of an intermediate representation for SDL called IF. In IF, 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.
Year
DOI
Venue
1999
10.1016/B978-044450228-5/50028-X
SDL'99: THE NEXT MILLENNIUM
Keywords
Field
DocType
SDL, time semantics, validation, model-checking, test generation, static analysis
Synchronization,Automata theory,Programming language,Abstraction,Model checking,Computer science,Automaton,Static analysis,Toolbox,Theoretical computer science,Intermediate language
Conference
Citations 
PageRank 
References 
37
2.60
15
Authors
7
Name
Order
Citations
PageRank
Marius Bozga12100127.83
Jean-claude Fernandez2372.60
Lucian Ghirvu320212.69
Susanne Graf440024.11
Jean-pierre Krimm516310.57
Laurent Mounier6118779.54
Joseph Sifakis76064814.75