{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T17:23:19Z","timestamp":1760548999207},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213147"},{"type":"electronic","value":"9783540247326"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24732-6_9","type":"book-chapter","created":{"date-parts":[[2010,7,28]],"date-time":"2010-07-28T00:14:47Z","timestamp":1280276087000},"page":"127-145","source":"Crossref","is-referenced-by-count":27,"title":["Validation of UML Models via a Mapping to Communicating Extended Timed Automata"],"prefix":"10.1007","author":[{"given":"Iulian","family":"Ober","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Susanne","family":"Graf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ileana","family":"Ober","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"http:\/\/www-omega.imag.fr - website of the IST OMEGA project"},{"key":"9_CR2","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)"},{"key":"9_CR3","volume-title":"Proceedings of 8th International Conference on Engineering of Complex Computer Systems","author":"V.D. Bianco","year":"2002","unstructured":"Bianco, V.D., Lavazza, L., Mauri, M.: Model checking UML specifications of real time software. In: Proceedings of 8th International Conference on Engineering of Complex Computer Systems, IEEE, Los Alamitos (2002)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Bornot, S., Sifakis, J.: An algebraic framework for urgency. Information and Computation, 163 (2000)","DOI":"10.1006\/inco.2000.2999"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/3-540-48119-2_19","volume-title":"FM\u201999 - Formal Methods","author":"M. Bozga","year":"1999","unstructured":"Bozga, M., Fernandez, J.C., Ghirvu, L., Graf, S., Krimm, J.P., Mounier, L.: IF: An intermediate representation and validation environment for timed asynchronous systems. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, p. 307. Springer, Heidelberg (1999)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/3-540-45657-0_26","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"2002","unstructured":"Bozga, M., Graf, S., Mounier, L.: IF-2.0: A validation environment for component-based real-time systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 343. Springer, Heidelberg (2002)"},{"key":"9_CR7","unstructured":"Bozga, M., Lesens, D., Mounier, L.: Model-Checking Ariane-5 Flight Program. In: Proceedings of FMICS 2001. pp. 211\u2013227. INRIA, Paris (2001)"},{"key":"9_CR8","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)"},{"key":"9_CR9","volume-title":"2001 IEEE International Symposium on Network Computing and Applications (NCA 2001)","author":"M. Bozga","year":"2001","unstructured":"Bozga, M., Graf, S., Mounier, L.: Automated validation of distributed software using the IF environment. In: 2001 IEEE International Symposium on Network Computing and Applications (NCA 2001), October 2001, IEEE, Los Alamitos (2001)"},{"key":"9_CR10","unstructured":"Bozga, M., Lakhnech, Y.: IF-2.0 common language operational semantics. Technical report, Deliverable of the IST Advance project, available from the authors (2002)"},{"key":"9_CR11","unstructured":"Graf, S., Hooman, J.: The Omega consortium. The Omega vision and workplan. Technical report, Omega Project deliverable (2003)"},{"key":"9_CR12","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":"2002","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 (2002)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/3-540-49213-5_8","volume-title":"Compositionality: The Significant Difference","author":"W. Damm","year":"1998","unstructured":"Damm, W., Josko, B., Hungar, H., Pnueli, A.: A compositional real-time semantics of STATEMATE designs. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 186\u2013238. Springer, Heidelberg (1998)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/3-540-45923-5_15","volume-title":"Fundamental Approaches to Software Engineering","author":"A. David","year":"2002","unstructured":"David, A., Oliver M\u00f6ller, M., Yi, W.: Formal Verification of UML Statecharts with Real-Time Extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol.\u00a02306, pp. 218\u2013232. Springer, Heidelberg (2002)"},{"issue":"2","key":"9_CR15","doi-asserted-by":"publisher","first-page":"101","DOI":"10.5381\/jot.2002.1.2.a1","volume":"1","author":"M. Mar Gallardo del","year":"2002","unstructured":"del Mar Gallardo, M., Merino, P., Pimentel, E.: Debugging UML designs with model checking. Journal of Object Technology\u00a01(2), 101\u2013117 (2002), http:\/\/www.jot.fm\/issues\/issue200207\/article1","journal-title":"Journal of Object Technology"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Graf, S., Ober, I.: A real-time profile for UML and how to adapt it to SDL. In: Proceedings of SDL Forum 2003, LNCS (2003) (to appear)","DOI":"10.1007\/3-540-45075-0_4"},{"key":"9_CR17","unstructured":"Graf, S., Jia, G.: Verification experiments on the MASCARA protocol. In: Proceedings of SPIN Workshop 2001, Toronto, Canada (January 2001)"},{"key":"9_CR18","unstructured":"Graf, S., Ober, I., Ober, I.: Timed annotations with UML. In: Proceedings of SVERTS 2003 (Satellite workshop of UML 2003), San-Francisco (2003), Available at http:\/\/www-verimag.imag.fr\/EVENTS\/2003\/SVERTS"},{"issue":"7","key":"9_CR19","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1109\/2.596624","volume":"30","author":"D. Harel","year":"1997","unstructured":"Harel, D., Gery, E.: Executable object modeling with statecharts. Computer\u00a030(7), 31\u201342 (1997)","journal-title":"Computer"},{"issue":"4","key":"9_CR20","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D. Harel","year":"1996","unstructured":"Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology\u00a05(4), 293\u2013333 (1996)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"9_CR21","volume-title":"Conference on System Science Engineering","author":"Z. Har\u2019El","year":"1988","unstructured":"Har\u2019El, Z., Kurshan, R.P.: Software for Analysis of Coordination. In: Conference on System Science Engineering, Pergamon Press, Oxford (1988)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The model-checker SPIN. IEEE Trans. on Software Engineering\u00a023(5) (1999)","DOI":"10.1109\/32.588521"},{"key":"9_CR23","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)"},{"issue":"3","key":"9_CR24","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1109\/32.4654","volume":"14","author":"C. Jard","year":"1988","unstructured":"Jard, C., Groz, R., Monin, J.F.: Development of VEDA, a prototyping tool for distributed algorithms. IEEE Transactions on Software Engineering\u00a014(3), 339\u2013352 (1988)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-45352-0_4","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"H. Jensen","year":"2000","unstructured":"Jensen, H., Larsen, K.G., Skou, A.: Scaling up Uppaal: Automatic verification of real-time systems using compositionality and abstraction. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol.\u00a01926, p. 19. Springer, Heidelberg (2000)"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-45739-9_23","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"A. Knapp","year":"2002","unstructured":"Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 395\u2013414. Springer, Heidelberg (2002)"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1007\/3-540-40011-7_39","volume-title":"UML 2000 - The Unified Modeling Language. Advancing the Standard","author":"G. Kwon","year":"2000","unstructured":"Kwon, G.: Rewrite rules and operational semantics for model checking UML statecharts. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000. LNCS, vol.\u00a01939, pp. 528\u2013540. Springer, Heidelberg (2000)"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioral subset of UML statechart diagrams using the SPiN model-checker. Formal Aspects of Computing\u00a0(11) (1999)","DOI":"10.1007\/s001659970003"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/3-540-46852-8_31","volume-title":"\u00abUML\u00bb \u201999 - The Unified Modeling Language. Beyond the Standard","author":"J. Lilius","year":"1999","unstructured":"Lilius, J., Paltor, I.P.: Formalizing UML state machines for model checking. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol.\u00a01723, pp. 430\u2013444. Springer, Heidelberg (1999)"},{"key":"9_CR30","volume-title":"Proceedings of 14th IEEE International Conference on Automated Software Engineering","author":"J. Lilius","year":"1999","unstructured":"Lilius, J., Paltor, I.P.: vUML: A tool for verifying UML models. In: Proceedings of 14th IEEE International Conference on Automated Software Engineering, IEEE, Los Alamitos (1999)"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63875-X_52","volume-title":"Advances in Computing Science - ASIAN\u201997","author":"E. Mikk","year":"1997","unstructured":"Mikk, E., Lakhnech, Y., Siegel, M.: Hierarchical automata as a model for statecharts. In: Shyamasundar, R.K. (ed.) ASIAN 1997. LNCS, vol.\u00a01345, Springer, Heidelberg (1997)"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of EUROPAR 1999","author":"I. Ober","year":"1999","unstructured":"Ober, I., Stan, I.: On the concurrent object model of UML. In: Proceedings of EUROPAR 1999. LNCS, Springer, Heidelberg (1999)"},{"key":"9_CR33","unstructured":"OMG. Unified Modeling Language Specification (Action Semantics). OMG Adopted Specification (December 2001)"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"OMG. Response to the OMG RFP for Schedulability, Performance and Time, v. 2.0. OMG ducument ad\/2002-03-04 (March 2002)","DOI":"10.1016\/S1351-4180(02)00809-7"},{"issue":"3","key":"9_CR35","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/S1571-0661(04)00262-2","volume":"55","author":"T. Sch\u00e4fer","year":"2001","unstructured":"Sch\u00e4fer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. Electronic Notes in Theoretical Computer Science\u00a055(3), 13 (2001)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9_CR36","unstructured":"WOODDES. Workshop on concurrency issues in UML. Satelite workshop of UML 2001 (2001), See http:\/\/wooddes.intranet.gr\/uml2001\/Home.htm"},{"key":"9_CR37","volume-title":"Proceedings of 16th IEEE International Conference on Automated Software Engineering (ASE 2001)","author":"F. Xie","year":"2001","unstructured":"Xie, F., Levin, V., Browne, J.C.: Model checking for an executable subset of UML. In: Proceedings of 16th IEEE International Conference on Automated Software Engineering (ASE 2001), IEEE, Los Alamitos (2001)"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Yovine, S.: Kronos: A verification tool for real-time systems. Springer International Journal of Software Tools for Technology Transfer\u00a01(1-2) (December 1997)","DOI":"10.1007\/s100090050009"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24732-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:29:53Z","timestamp":1559330993000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24732-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213147","9783540247326"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24732-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}