Abstract
It is widely recognised that the automated validation of complex systems can hardly be achieved without tool integration. The development of the IF-1.0 toolbox [3] was initiated several years ago, in order to provide an open validation platform for timed asynchronous systems (such as telecommunication protocols or distributed applications, in general). The toolbox was built upon an intermediate representation language based on extended timed automata. In particular, this representation allowed us to study the semantics of real-time primitives for asynchronous systems. Currently, the toolbox contains dedicated tools on the intermediate language (such as compilers, static analysers and model-checkers) as well as front-ends to various specification languages and validation tools (academic and commercial ones). Among the dedicated tools, we focused on static analysis (such as slicing and abstraction) which are mandatory for an automated validation of complex systems. Finally, the toolbox was successfully used on several case studies, the most relevant ones being presented in [4].
This work was supported in part by the European Commission FET projects ADVANCE, contract No IST-1999-29082 and AGEDIS, contract No IST-1999-20218
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
K. Altisen, G. Gößler, and J. Sifakis. A Methodology for the Construction of Scheduled Systems. In Mathai Joseph, editor, Proceedings of FTRTFT 2000, number 1926 in LNCS, pages 106–120. Springer-Verlag, September 2000.
S. Bornot, J. Sifakis, and S. Tripakis. Modeling Urgency in Timed Systems. In International Symposium: Compositionality-The Significant Difference (Holstein, Germany), volume 1536 of LNCS. Springer, September 1997.
M. Bozga, J.Cl. Fernandez, L. Ghirvu, S. Graf, J. P. Krimm, and L. Mounier. IF: A Validation Environment for Timed Asynchronous Systems. In E. A. Emerson and A. P. Sistla, editors, Proceedings of CAV’00 (Chicago, USA), volume 1855 of LNCS. Springer, July 2000.
M. Bozga, S. Graf, and L. Mounier. Automated Validation of Distributed Software using the IF Environment. In Workshop on Software Model-Checking, volume 55. TCS, July 2001.
H. Garavel. OPEN/CÆSAR: An Open Software Architecture for Verification, Simulation, and Testing. In B. Steffen, editor, Proceedings of TACAS’98 (Lisbon, Portugal), volume 1384 of LNCS, pages 68–84. Springer, March 1998.
P. Godefroid. VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software (short paper). In Proceedings of CAV’97 (Haifa, Israel), volume 1254 of LNCS, pages 476–479. Springer, June 1997.
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall Software Series, http://cm.bell-labs.com/cm/cs/what/spin, 1991.
ITU-T. Recommendation Z.100. Specification and Description Language (SDL). Technical Report Z-100, International Telecommunication Union-Standardization Sector, Genève, November 1999.
T. Jéron and P. Morel. Test Generation Derived from Model Checking. In N. Halb-wachs and D. Peled, editors, Proceedings of CAV’99 (Trento, Italy), volume 1633 of LNCS, pages 108–122. Springer, July 1999.
OMG. Unified Modeling Language Specification. Technical Report OMG UML v1.3-ad/99-06-09, Object Management Group, June 1999.
S. Swan. An Introduction to System-Level Modeling in Systemc 2.0. Technical report, Open SystemC Initiative, 2001.
W. Visser, K. Havelund, G. Brat, and S. Park. Model checking programs. In Proceedings of ASE’00. IEEE Computer Society, September 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bozga, M., Graf, S., Mounier, L. (2002). IF-2.0: A Validation Environment for Component-Based Real-Time Systems. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_26
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive