{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T12:47:41Z","timestamp":1780490861788,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540230687","type":"print"},{"value":"9783540300809","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30080-9_8","type":"book-chapter","created":{"date-parts":[[2010,9,7]],"date-time":"2010-09-07T03:26:49Z","timestamp":1283830009000},"page":"237-267","source":"Crossref","is-referenced-by-count":69,"title":["The IF Toolset"],"prefix":"10.1007","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Susanne","family":"Graf","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ileana","family":"Ober","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Iulian","family":"Ober","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joseph","family":"Sifakis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/3-540-44585-4_34","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2001","unstructured":"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.\u00a02102, p. 368. Springer, Heidelberg (2001)"},{"key":"8_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/3-540-45352-0_11","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"K. Altisen","year":"2000","unstructured":"Altisen, K., G\u00f6ssler, G., Sifakis, J.: A Methodology for the Construction of Scheduled Systems. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol.\u00a01926, pp. 106\u2013120. Springer, Heidelberg (2000)"},{"issue":"1\/2","key":"8_CR4","first-page":"55","volume":"23","author":"K. Altisen","year":"2002","unstructured":"Altisen, K., G\u00f6ssler, G., Sifakis, J.: Scheduler Modeling Based on the Controller Snthesis Paradigm. Journal of Real-Time Systems, special issue on \u201ccontrol-theoretical approaches to real-time computing\u201d\u00a023(1\/2), 55\u201384 (2002)","journal-title":"Journal of Real-Time Systems, special issue on \u201ccontrol-theoretical approaches to real-time computing\u201d"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"1991","unstructured":"Bouajjani, A., Fernandez, J.C., Graf, S., Rodriguez, C., Sifakis, J.: Safety for Branching Time Semantics. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, Springer, Heidelberg (1991)"},{"key":"8_CR6","first-page":"423","volume-title":"Proceedings of SDL FORUM 1999","author":"M. Bozga","year":"1999","unstructured":"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\u2013440. Elsevier, Amsterdam (1999)"},{"issue":"1+2","key":"8_CR7","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/s100090050012","volume":"1","author":"M. Bozga","year":"1997","unstructured":"Bozga, M., Fernandez, J.C., Kerbrat, A., Mounier, L.: Protocol Verification with the Aldebaran Toolset. Software Tools for Technology Transfer\u00a01(1+2), 166\u2013183 (1997)","journal-title":"Software Tools for Technology Transfer"},{"key":"8_CR8","unstructured":"Boigelot, B., Latour, L.: The Liege Automata-based Symbolic Handler LASH (2002), \n                    \n                      http:\/\/www.montefiore.ulg.ac.be\/boigelot\/research\/lash"},{"key":"8_CR9","unstructured":"Bozga, M., Lakhnech, Y.: IF-2.0: Common Language Operational Semantics. Technical report, Verimag (2002)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"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.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.2000.2999","volume":"163","author":"S. Bornot","year":"2000","unstructured":"Bornot, S., Sifakis, J.: An Algebraic Framework for Urgency. Information and Computatio\u00a0163, 172\u2013202 (2000)","journal-title":"Information and Computatio"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-49213-5_5","volume-title":"Compositionality: The Significant Difference","author":"S. Bornot","year":"1998","unstructured":"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.\u00a01536, p. 103. Springer, Heidelberg (1998)"},{"key":"8_CR13","unstructured":"ADVANCE Consortium, \n                    \n                      http:\/\/www.liafa.jussieu.fr\/\n                    \n                    \n                   advance - website of the IST ADVANCE project (2001)"},{"key":"8_CR14","unstructured":"AGEDIS Consortium, \n                    \n                      http:\/\/www.agedis.de\n                    \n                    \n                   - website of the IST AGEDIS project (2002)"},{"key":"8_CR15","unstructured":"OMEGA Consortium, \n                    \n                      http:\/\/www-omega.imag.fr\n                    \n                    \n                   - website of the IST OMEGA project. (2003)"},{"key":"8_CR16","volume-title":"FMOODS 1999 IFIP TC6\/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems","author":"W. Damm","year":"1999","unstructured":"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)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-39656-7_3","volume-title":"Formal Methods for Components and Objects","author":"W. Damm","year":"2003","unstructured":"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.\u00a02852, pp. 71\u201398. Springer, Heidelberg (2003)"},{"key":"8_CR18","first-page":"73","volume-title":"Proceedings of RTSS 1996","author":"C. Daws","year":"1996","unstructured":"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\u201382. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"Computer Aided Verification","author":"J.C. Fernandez","year":"1996","unstructured":"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.\u00a01102, pp. 437\u2013440. Springer, Heidelberg (1996)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"J.C. Fernandez","year":"1996","unstructured":"Fernandez, J.C., Jard, C., J\u00e9ron, 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.\u00a01102, Springer, Heidelberg (1996)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-540-24769-2_21","volume-title":"Software Architecture","author":"S. Graf","year":"2004","unstructured":"Graf, S., Hooman, J.: Correct development of embedded systems. In: Oquendo, F., Warboys, B.C., Morrison, R. (eds.) EWSA 2004. LNCS, vol.\u00a03047, pp. 241\u2013249. Springer, Heidelberg (2004)"},{"key":"8_CR22","unstructured":"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 \n                    \n                      http:\/\/wwwverimag.imag.fr\/EVENTS\/2003\/SVERTS\/"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-39656-7_19","volume-title":"Formal Methods for Components and Objects","author":"G. G\u00f6ssler","year":"2003","unstructured":"G\u00f6ssler, 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.\u00a02852, pp. 443\u2013466. Springer, Heidelberg (2003)"},{"key":"8_CR24","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Sci. Comput. Programming\u00a08, 231\u2013274 (1987)","journal-title":"Sci. Comput. Programming"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Hartman, A., Nagin, K.: The AGEDIS Tools for Model Based Testing. In: Proceedings of ISSTA 2004 (2004)","DOI":"10.1145\/1007512.1007529"},{"key":"8_CR26","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall Software Series (1991)"},{"key":"8_CR27","volume-title":"Modeling Reactive Systems with Statecharts: The STATEMATE Approach","author":"D. Harel","year":"1998","unstructured":"Harel, D., Politi, M.: Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, New York (1998)"},{"key":"8_CR28","unstructured":"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)"},{"key":"8_CR29","unstructured":"IBM. Rational ROSE Development Environment"},{"key":"8_CR30","unstructured":"Ilogix. Rhapsody Development Environment"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-48683-6_12","volume-title":"Computer Aided Verification","author":"T. J\u00e9ron","year":"1999","unstructured":"J\u00e9ron, T., Morel, P.: Test Generation Derived from Model Checking. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 108\u2013122. Springer, Heidelberg (1999)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Results on the Propositional \u03bc-Calculus. Theoretical Computer Science (1983)","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"8_CR33","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1998","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. Journal on Software Tools for Technology Transfer\u00a01, 134\u2013152 (1998)","journal-title":"Journal on Software Tools for Technology Transfer"},{"key":"8_CR34","unstructured":"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)"},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communication Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communication Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"key":"8_CR36","volume-title":"Advanced Compiler Design Implementation","author":"S. Muchnick","year":"1997","unstructured":"Muchnick, S.: Advanced Compiler Design Implementation. Morgan Kaufmann Publishers, San Francisco (1997)"},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"X. Nicollin","year":"1992","unstructured":"Nicollin, X., Sifakis, J.: An Overview and Synthesis on Timed Process Algebras. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol.\u00a0575, Springer, Heidelberg (1992)"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-540-24732-6_9","volume-title":"Model Checking Software","author":"I. Ober","year":"2004","unstructured":"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.\u00a02989, pp. 127\u2013145. Springer, Heidelberg (2004)"},{"key":"8_CR39","unstructured":"OMG. Unified Modeling Language Specification (Action Semantics). OMG Adopted Specification (December 2001)"},{"key":"8_CR40","unstructured":"OMG. Model Driven Architecture (2003), \n                    \n                      http:\/\/www.omg.org\/mda"},{"key":"8_CR41","unstructured":"OMG. Standard uml Profile for Schedulability, Performance and Time, v. 1.0. OMG document formal\/2003-09-01 (September 2003)"},{"key":"8_CR42","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume":"104","author":"D. Park","year":"1981","unstructured":"Park, D.: Concurrency and Automata on Infinite Sequences. Theoretical Computer Science\u00a0104, 167\u2013183 (1981)","journal-title":"Theoretical Computer Science"},{"key":"8_CR43","unstructured":"Ramirez, A., Vanpeperstraete, P., Rueckert, A., Odutola, K., Bennett, J., Tolke, L.: ArgoUML Environment"},{"key":"8_CR44","unstructured":"Sifakis, J.: Use of Petri Nets for Performance Evaluation. In: Proc. 3rd Intl. Symposium on Modeling and Evaluation, pp. 75\u201393. IFIP, North Holland (1977)"},{"key":"8_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/3-540-45449-7_26","volume-title":"Embedded Software","author":"J. Sifakis","year":"2001","unstructured":"Sifakis, J.: Modeling Real-Time Systems \u2014 Challenges and Work Directions. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol.\u00a02211, p. 373. Springer, Heidelberg (2001)"},{"issue":"1","key":"8_CR46","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/JPROC.2002.805820","volume":"91","author":"J. Sifakis","year":"2003","unstructured":"Sifakis, J., Tripakis, S., Yovine, S.: Building Models of Real-Time Systems from Application Software. Proc. IEEE\u00a091(1), 100\u2013111 (2003)","journal-title":"Proc. IEEE"},{"key":"8_CR47","unstructured":"Tip, F.: A Survey of Program Slicing Techniques. Technical Report CSR9438, CWI, Amsterdam, The Netherlands (1994)"},{"key":"8_CR48","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching-Time and Abstraction in Bisimulation Semantics. Technical Report CS-R8911, CWI, Amsterdam, The Netherlands (1989)"},{"issue":"4","key":"8_CR49","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"SE-10","author":"M. Weiser","year":"1984","unstructured":"Weiser, M.: Program Slicing. IEEE Transactions on Software Engineering\u00a0SE-10(4), 352\u2013357 (1984)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1+2","key":"8_CR50","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: KRONOS: A Verification Tool for Real-Time Systems. Software Tools for Technology Transfer\u00a01(1+2), 123\u2013133 (1997)","journal-title":"Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for the Design of Real-Time Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30080-9_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:44:26Z","timestamp":1620013466000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30080-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230687","9783540300809"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30080-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}