Abstract
This paper presents an overview on the IF toolset which is an environment for modelling and validation of heterogeneous real-time systems. The toolset is built upon a rich formalism, the IF notation, allowing structured automata-based system representations. Moreover, the IF notation is expressive enough to support real-time primitives and extensions of high-level modelling languages such as SDL and UML by means of structure preserving mappings.
The core part of the IF toolset consists of a syntactic transformation component and an open exploration platform. The syntactic transformation component provides language level access to IF descriptions and has been used to implement static analysis and optimisation techniques. The exploration platform gives access to the graph of possible executions. It has been connected to different state-of-the-art model-checking and test-case generation tools.
A methodology for the use of the toolset is presented at hand of a case study concerning the Ariane-5 Flight Program for which both an SDL and a UML model have been validated.
This work was supported in part by the European Commission through the projects IST-1999-29082 ADVANCE, IST-1999-20218 AGEDIS and IST-2001-33522 OMEGA.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: A Tool for Reachability Analysis of Complex Systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 368. Springer, Heidelberg (2001)
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)
Altisen, K., Gössler, G., Sifakis, J.: A Methodology for the Construction of Scheduled Systems. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 106–120. Springer, Heidelberg (2000)
Altisen, K., Gössler, G., Sifakis, J.: Scheduler Modeling Based on the Controller Snthesis Paradigm. Journal of Real-Time Systems, special issue on “control-theoretical approaches to real-time computing” 23(1/2), 55–84 (2002)
Bouajjani, A., Fernandez, J.C., Graf, S., Rodriguez, C., Sifakis, J.: Safety for Branching Time Semantics. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, Springer, Heidelberg (1991)
Bozga, M., Fernandez, J.C., Ghirvu, L., Graf, S., Krimm, J.P., Mounier, L., Sifakis, J.: IF: An Intermediate Representation for SDL and its Applications. In: Dssouli, R., Bochmann, G., Lahav, Y. (eds.) Proceedings of SDL FORUM 1999, Montreal, Canada, June 1999, pp. 423–440. Elsevier, Amsterdam (1999)
Bozga, M., Fernandez, J.C., Kerbrat, A., Mounier, L.: Protocol Verification with the Aldebaran Toolset. Software Tools for Technology Transfer 1(1+2), 166–183 (1997)
Boigelot, B., Latour, L.: The Liege Automata-based Symbolic Handler LASH (2002), http://www.montefiore.ulg.ac.be/boigelot/research/lash
Bozga, M., Lakhnech, Y.: IF-2.0: Common Language Operational Semantics. Technical report, Verimag (2002)
Bensalem, S., Lakhnech, Y., Owre, S.: Computing Abstractions of Infinite State Systems Compositionally and Automatically. In: Hu, A., Vardi, M. (eds.) CAV 1998. LNCS, vol. 1427, pp. 319–331. Springer, Heidelberg (1998)
Bornot, S., Sifakis, J.: An Algebraic Framework for Urgency. Information and Computatio 163, 172–202 (2000)
Bornot, S., Sifakis, J., Tripakis, S.: Modeling Urgency in Timed Systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, p. 103. Springer, Heidelberg (1998)
ADVANCE Consortium, http://www.liafa.jussieu.fr/ advance - website of the IST ADVANCE project (2001)
AGEDIS Consortium, http://www.agedis.de - website of the IST AGEDIS project (2002)
OMEGA Consortium, http://www-omega.imag.fr - website of the IST OMEGA project. (2003)
Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. In: Ciancarini, P., Fantechi, A., Gorrieri, R. (eds.) FMOODS 1999 IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems, Kluwer Academic Publishers, Dordrecht (1999); Journal Version to appear in Journal on Formal Methods in System Design (July 2001)
Damm, W., Josko, B., Pnueli, A., Votintseva, A.: Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 71–98. Springer, Heidelberg (2003)
Daws, C., Yovine, S.: Reducing the Number of Clock Variables of Timed Automata. In: Proceedings of RTSS 1996, Washington, DC, USA, December 1996, pp. 73–82. IEEE Computer Society Press, Los Alamitos (1996)
Fernandez, J.C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., Sighireanu, M.: CADP: A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 437–440. Springer, Heidelberg (1996)
Fernandez, J.C., Jard, C., Jéron, T., Viho, C.: Using On-the-fly Verification Techniques for the Generation of Test Suites. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)
Graf, S., Hooman, J.: Correct development of embedded systems. In: Oquendo, F., Warboys, B.C., Morrison, R. (eds.) EWSA 2004. LNCS, vol. 3047, pp. 241–249. Springer, Heidelberg (2004)
Graf, S., Ober, I., Ober, I.: Timed Annotations in UML. In: Workshop SVERTS on Specification and Validation of UML models for Real Time and Embedded Systems, a satellite event of UML 2003, San Francisco (October 2003), Verimag technical report 2003/10/22 or http://wwwverimag.imag.fr/EVENTS/2003/SVERTS/
Gössler, G., Sifakis, J.: Composition for Component-Based Modeling. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 443–466. Springer, Heidelberg (2003)
Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Sci. Comput. Programming 8, 231–274 (1987)
Hartman, A., Nagin, K.: The AGEDIS Tools for Model Based Testing. In: Proceedings of ISSTA 2004 (2004)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall Software Series (1991)
Harel, D., Politi, M.: Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, New York (1998)
Hooman, J., van der Zwaag, M.B.: A Semantics of Communicating Reactive Objects with Timing. In: Proceedings of SVERTS 2003 (Specification and Validation of UML models for Real Time and Embedded Systems), San Francisco (October 2003)
IBM. Rational ROSE Development Environment
Ilogix. Rhapsody Development Environment
Jéron, T., Morel, P.: Test Generation Derived from Model Checking. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 108–122. Springer, Heidelberg (1999)
Kozen, D.: Results on the Propositional μ-Calculus. Theoretical Computer Science (1983)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. Journal on Software Tools for Technology Transfer 1, 134–152 (1998)
Lugato, D., Rapin, N., Gallois, J.P.: Verification and tests generation for SDL industrial specifications with the AGATHA toolset. In: Real-Time Tools Workshop affiliated to CONCUR 2001, Aalborg, Denmark (2001)
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Muchnick, S.: Advanced Compiler Design Implementation. Morgan Kaufmann Publishers, San Francisco (1997)
Nicollin, X., Sifakis, J.: An Overview and Synthesis on Timed Process Algebras. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, Springer, Heidelberg (1992)
Ober, I., Graf, S., Ober, I.: Model Checking of UML Models via a Mapping to Communicating Extended Timed Automata. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 127–145. Springer, Heidelberg (2004)
OMG. Unified Modeling Language Specification (Action Semantics). OMG Adopted Specification (December 2001)
OMG. Model Driven Architecture (2003), http://www.omg.org/mda
OMG. Standard uml Profile for Schedulability, Performance and Time, v. 1.0. OMG document formal/2003-09-01 (September 2003)
Park, D.: Concurrency and Automata on Infinite Sequences. Theoretical Computer Science 104, 167–183 (1981)
Ramirez, A., Vanpeperstraete, P., Rueckert, A., Odutola, K., Bennett, J., Tolke, L.: ArgoUML Environment
Sifakis, J.: Use of Petri Nets for Performance Evaluation. In: Proc. 3rd Intl. Symposium on Modeling and Evaluation, pp. 75–93. IFIP, North Holland (1977)
Sifakis, J.: Modeling Real-Time Systems — Challenges and Work Directions. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, p. 373. Springer, Heidelberg (2001)
Sifakis, J., Tripakis, S., Yovine, S.: Building Models of Real-Time Systems from Application Software. Proc. IEEE 91(1), 100–111 (2003)
Tip, F.: A Survey of Program Slicing Techniques. Technical Report CSR9438, CWI, Amsterdam, The Netherlands (1994)
van Glabbeek, R.J., Weijland, W.P.: Branching-Time and Abstraction in Bisimulation Semantics. Technical Report CS-R8911, CWI, Amsterdam, The Netherlands (1989)
Weiser, M.: Program Slicing. IEEE Transactions on Software Engineering SE-10(4), 352–357 (1984)
Yovine, S.: KRONOS: A Verification Tool for Real-Time Systems. Software Tools for Technology Transfer 1(1+2), 123–133 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bozga, M., Graf, S., Ober, I., Ober, I., Sifakis, J. (2004). The IF Toolset. In: Bernardo, M., Corradini, F. (eds) Formal Methods for the Design of Real-Time Systems. SFM-RT 2004. Lecture Notes in Computer Science, vol 3185. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30080-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-30080-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23068-7
Online ISBN: 978-3-540-30080-9
eBook Packages: Springer Book Archive