{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T06:53:51Z","timestamp":1760424831007},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441656"},{"type":"electronic","value":"9783540457398"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45739-9_23","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T22:42:01Z","timestamp":1179268921000},"page":"395-414","source":"Crossref","is-referenced-by-count":104,"title":["Model Checking Timed UML State Machines and Collaborations"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Knapp","sequence":"first","affiliation":[]},{"given":"Stephan","family":"Merz","sequence":"additional","affiliation":[]},{"given":"Christopher","family":"Rauh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,10,4]]},"reference":[{"key":"23_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Rajeev Alur and David L. Dill. A Theory of Timed Automata. Theo. Comp. Sci., 126:183\u2013235, 1994.","journal-title":"Theo. Comp. Sci."},{"key":"23_CR2","unstructured":"Rodolphe Arthaud, Udo Brockmeyer, Werner Damm, Bruce P. Douglass, Francois Terrier, and Wang Yi, editors. Proc. Wsh. Formal Design Techniques for Real-Time UML, York, 2000. http:\/\/wooddes.intranet.gr\/workshop.htm ."},{"key":"23_CR3","volume-title":"The Unified Modeling Language User Guide","author":"G. Booch","year":"1998","unstructured":"Grady Booch, James Rumbaugh, and Ivar Jacobson. The Unified Modeling Language User Guide. Addison-Wesley, Reading, Mass., &c, 1998."},{"issue":"1","key":"23_CR4","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1023\/A:1011227529550","volume":"19","author":"W. Damm","year":"2001","unstructured":"Werner Damm and David Harel. LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design, 19(1):45\u201380, 2001.","journal-title":"Formal Methods in System Design"},{"key":"23_CR5","series-title":"Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/3-540-49213-5_8","volume-title":"Proc. Int. Symp. Compositionality (Revised Lectures)","author":"W. Damm","year":"1998","unstructured":"Werner Damm, Bernhard Josko, Hardi Hungar, and Amir Pnueli. A Compositional Real-Time Semantics of STATEMATE Designs. In Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli, editors, Proc. Int. Symp. Compositionality (Revised Lectures), volume 1536 of Lect. Notes Comp. Sci., pages 186\u2013238. Springer, Berlin, 1998."},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Alexandre David and M. Oliver M\u00f6ller. From HUppaal to Uppaal \u2014 A Translation from Hierarchical Timed Automata to Flat Timed Automata. Technical Report BRICS RS-01-11, Department of Computer Science, Aarhus Universitet, 2001.","DOI":"10.7146\/brics.v8i11.20467"},{"key":"23_CR7","volume-title":"Real-Time UML","author":"B. P. Douglass","year":"1998","unstructured":"Bruce P. Douglass. Real-Time UML. Addison-Wesley, Reading, Mass., &c., 1998."},{"key":"23_CR8","series-title":"Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"645","DOI":"10.1007\/3-540-46852-8_45","volume-title":"Proc. 2nd Int. Conf. UML","author":"T. Firley","year":"1999","unstructured":"Thomas Firley, Michaela Huhn, Karsten Diethers, Thomas Gehrke, and Ursula Goltz. Timed Sequence Diagrams and Tool-Based Analysis \u2014 A Case Study. In Bernhard Rumpe, editors. Proc. 2 nd Int. Conf. UML, volume 1723 of Lect. Notes Comp. Sci. Springer, Berlin, 1999 France and Rumpe [9], pages 645\u2013660."},{"key":"23_CR9","series-title":"Lect. Notes Comp. Sci.","volume-title":"Proc. 2nd Int. Conf. UML","year":"1999","unstructured":"Robert B. France and Bernhard Rumpe, editors. Proc. 2 nd Int. Conf. UML, volume 1723 of Lect. Notes Comp. Sci. Springer, Berlin, 1999."},{"issue":"3","key":"23_CR10","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"David Harel. Statecharts: A Visual Formalism for Complex Systems. Sci. Comp. Program., 8(3):231\u2013274, 1987.","journal-title":"Sci. Comp. Program."},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"David Harel and Eran Grey. Executable Object Modeling with Statecharts. Computer, July:31\u201342, 1997.","DOI":"10.1109\/2.596624"},{"key":"23_CR12","unstructured":"Constance L. Heitmeyer, Ralph D. Jeffords, and Bruce G. Labaw. Comparing Different Approaches for Specifying and Verifying Real-Time Systems. In Proc. 10 th IEEE Wsh. Real-Time Operating Systems and Software, pages 122\u2013129, New York, 1993."},{"issue":"1\u20132","key":"23_CR13","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a Nutshell. Int. J. Softw. Tools for Techn. Transfer, 1(1\u20132):134\u2013152, 1997.","journal-title":"Int. J. Softw. Tools for Techn. Transfer"},{"issue":"6","key":"23_CR14","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11","author":"D. Latella","year":"1999","unstructured":"Diego Latella, Istvan Majzik, and Mieke Massink. Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-Checker. Formal Aspects Comp., 11(6):637\u2013664, 1999.","journal-title":"Formal Aspects Comp."},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Luigi Lavazza, Gabriele Quaroni, and Matteo Venturelli. Combining UML and Formal Notations for Modelling Real-Time Systems. In 8 th Europ. Conf. Software Engineering, Wien, 2001.","DOI":"10.1145\/503209.503236"},{"key":"23_CR16","series-title":"Lect. Notes Comp. Sci.","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/3-540-46852-8_31","volume-title":"Proc. 2nd Int. Conf. UML","author":"J. Lilius","year":"1999","unstructured":"Johan Lilius and Iv\u00e1n Porres Paltor. Formalising UML State Machines for Model Checking. In Bernhard Rumpe, editors. Proc. 2 nd Int. Conf. UML, volume 1723 of Lect. Notes Comp. Sci. Springer, Berlin, 1999 France and Rumpe [9], pages 430\u2013445."},{"key":"23_CR17","series-title":"PhD thesis","volume-title":"Real-Time Reactive System Development \u2014 A Formal Approach Based on UML and PVS","author":"D. Muthiayen","year":"2000","unstructured":"Darmalingum Muthiayen. Real-Time Reactive System Development \u2014 A Formal Approach Based on UML and PVS. PhD thesis, Concordia University, Montreal, Canada, 2000."},{"key":"23_CR18","unstructured":"Object Management Group. Unified Modeling Language Specification, Version 1.4. Specification, OMG, 2001. http:\/\/cgi.omg.org\/cgi-bin\/doc?formal\/01-09-67 ."},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"Timm Sch\u00e4fer, Alexander Knapp, and Stephan Merz. Model Checking UML State Machines and Collaborations. In Scott Stoller and Willem Visser, editors, Proc. Wsh. Software Model Checking, volume 55(3) of Elect. Notes Theo. Comp. Sci., Paris, 2001. 13 pages.","DOI":"10.1016\/S1571-0661(04)00262-2"},{"key":"23_CR20","volume-title":"Real-Time Object-Oriented Modeling","author":"B. Selic","year":"1994","unstructured":"Bran Selic, Garth Gullekson, and Paul T. Ward. Real-Time Object-Oriented Modeling. John Wiley & Sons, New York, 1994."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45739-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T20:54:35Z","timestamp":1556398475000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45739-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441656","9783540457398"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45739-9_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}