{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:50:18Z","timestamp":1725558618690},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203032"},{"type":"electronic","value":"9783540396567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39656-7_4","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T14:35:52Z","timestamp":1277822152000},"page":"99-135","source":"Crossref","is-referenced-by-count":9,"title":["Live and Let Die: LSC-Based Verification of UML-Models"],"prefix":"10.1007","author":[{"given":"Werner","family":"Damm","sequence":"first","affiliation":[]},{"given":"Bernd","family":"Westphal","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1\/2","key":"4_CR1","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting Symmetry in Temporal Logic Model Checking. Formal Methods in System Design\u00a09(1\/2), 77\u2013104 (1996)","journal-title":"Formal Methods in System Design"},{"key":"4_CR2","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/10722468_13","volume-title":"SPIN Model Checking and Software Verification","author":"J. Corbett","year":"2000","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Robby: A Language Framework for Expressing Checkable Properties of Dynamic Software. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 205\u2013223. Springer, Heidelberg (2000)"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Csert\u00e1n, G., Huszerl, G., Majzik, I., Pap, Z., Pataricza, A., Varr\u00f3, D.: Viatra - visual automated transformations for formal verification of uml models. In: Proceedings International Conference on Automated Software Engineering, ASE 2002 (2002)","DOI":"10.1109\/ASE.2002.1115027"},{"issue":"1","key":"4_CR5","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1023\/A:1011279932612","volume":"19","author":"W. Damm","year":"2001","unstructured":"Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design\u00a019(1), 121\u2013141 (2001)","journal-title":"Formal Methods in System Design"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Damm, W., Jonsson, B.: Eliminating Queues from RT UML Model Representations. In: Damm and Olderog [8], pp. 375\u2013394","DOI":"10.1007\/3-540-45739-9_22"},{"key":"4_CR7","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":"4_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","year":"2002","unstructured":"Damm, W., Olderog, E.-R. (eds.): FTRTFT 2002. LNCS, vol.\u00a02469. Springer, Heidelberg (2002)"},{"key":"4_CR9","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., M\u00f6ller, M.O., 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":"1\/2","key":"4_CR10","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and Model Checking. Formal Methods in System Design\u00a09(1\/2), 105\u2013131 (1996)","journal-title":"Formal Methods in System Design"},{"volume-title":"Proceedings of ASE2001 (16th IEEE International Conference on Automated Software Engineering)","year":"2001","key":"4_CR11","unstructured":"Feather, M., Goedicke, M. (eds.): Proceedings of ASE2001 (16th IEEE International Conference on Automated Software Engineering). IEEE CS Press, Los Alamitos (November 2001)"},{"key":"4_CR12","unstructured":"Le Guennec, A.: Genie Logiciel et Methodes Formelles avec UML - Specification, Validation et Generation de Tests. PhD thesis, Universit\u00e9 de Rennes 1 (2001)"},{"issue":"7","key":"4_CR13","doi-asserted-by":"crossref","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. IEEE Computer\u00a030(7), 31\u201342 (1997)","journal-title":"IEEE Computer"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Harel, D., Marelly, R.: Specifying and executing behavioral requirements: The play-in\/ play-out approach. Technical Report MCS01-15, The Weizmann Institute of Science (2001)","DOI":"10.1145\/985072.985115"},{"key":"4_CR15","unstructured":"Hussmann, H.: Loose semantics for uml,ocl. In: Proceedings 6th World Conference on Integrated Design & Process Technology (IDPT 2002). Society for Design and Process Science (June 2002)"},{"key":"4_CR16","volume-title":"Proceedings of ASE-2001: The 16th IEEE Conference on Automated Software Engineering","author":"R. Iosif","year":"2001","unstructured":"Iosif, R.: Exploiting heap symmetries in explicit-state model checking of software. In: Feather, M., Goedicke, M. (eds.) Proceedings of ASE-2001: The 16th IEEE Conference on Automated Software Engineering. IEEE CS Press, Los Alamitos (November 2001)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-46017-9_5","volume-title":"Model Checking Software","author":"R. Iosif","year":"2002","unstructured":"Iosif, R.: Symmetry reduction criteria for software model checking. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 22\u201341. Springer, Heidelberg (2002)"},{"issue":"1\/2","key":"4_CR18","first-page":"41","volume":"9","author":"C.N. Ip","year":"1996","unstructured":"Ip, C.N., Dill, D.L.: Better Verification Through Symmetry. Formal Methods in System Design\u00a09(1\/2), 41\u201375 (1996)","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"4_CR19","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1023\/A:1008723125149","volume":"14","author":"C.N. Ip","year":"1999","unstructured":"Ip, C.N., Dill, D.L.: Verifying Systems with Replicated Components in Mur\u03c6. Formal Methods in System Design\u00a014(3), 273\u2013310 (1999)","journal-title":"Formal Methods in System Design"},{"key":"4_CR20","unstructured":"ITU-T. ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU-T, Geneva (1993)"},{"key":"4_CR21","unstructured":"ITU-T. ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU-T, Geneva (1996)"},{"key":"4_CR22","unstructured":"ITU-T. ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU-T, Geneva (1999)"},{"key":"4_CR23","unstructured":"Kleppe, A., Warmer, J.: Unification of static and dynamic semantics of uml. Technical report, Klasse Objecten, Soest, Netherlands (2001)"},{"key":"4_CR24","unstructured":"Klose, J.: Syntax and Semantics of Live Sequence Charts. PhD thesis, Carl von Ossietzky Universit\u00e4t Oldenburg (2003) (to appear)"},{"key":"4_CR25","unstructured":"Klose, J., Westphal, B.: Relating LSC Specifications to UML Models. In: Ehrig, H., Grosse-Rhode, M. (eds.) Proceedings INT2002- International Workshop on Integration of Specification Techniques for Applications in Engineering (April 2002)"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/3-540-45319-9_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Klose","year":"2001","unstructured":"Klose, J., Wittke, H.: An Automata Based Interpretation of Live Sequence Charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 512\u2013527. Springer, Heidelberg (2001)"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Knapp, A., Merz, S., Rauh, C.: Model Checking Timed UML State Machines and Collaborations. In: Damm and Olderog [8], pp. 395\u2013416","DOI":"10.1007\/3-540-45739-9_23"},{"issue":"6","key":"4_CR28","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11","author":"D. Latella","year":"1999","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\u00a011(6), 637\u2013664 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"4_CR29","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1991)"},{"key":"4_CR30","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/582419.582429","volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002","author":"R. Marelly","year":"2002","unstructured":"Marelly, R., Harel, D., Kugler, H.: Multiple instances and symbolic variables in executable sequence charts. In: Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, Seattle, Washington, USA, November 4-8. SIGPLAN Notices, vol.\u00a037(11), pp. 83\u2013100. ACM, New York (2002)"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1998","unstructured":"McMillan, K.L.: Verification of an Implementation of Tomasulo\u2019s Algorithm by Compositional Model Checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol.\u00a01427, pp. 110\u2013121. Springer, Heidelberg (1998)"},{"key":"4_CR32","unstructured":"McMillan, K.L.: Getting Started with SMV. Technical report, Cadence Berkeley Labs (March 1999), http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/tutorial.ps"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods","author":"K.L. McMillan","year":"1999","unstructured":"McMillan, K.L.: Verification of Infinite State Systems by Compositional Model Checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 219\u2013233. Springer, Heidelberg (1999)"},{"key":"4_CR34","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0167-6423(99)00030-1","volume":"37","author":"K.L. McMillan","year":"2000","unstructured":"McMillan, K.L.: A Methodology for Hardware Verification using Compositional Model Checking. Science of Computer Programming\u00a037, 279\u2013309 (2000)","journal-title":"Science of Computer Programming"},{"key":"4_CR35","unstructured":"Ober, I.: Harmonizing Design Languages with Object-Oriented Extensions and an Executable Semantics. PhD thesis, Institut National Polytechnique de Toulouse (April 2001)"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Ober, I.: An asm semantics of uml derived from the meta-model and incorporating actions. In: B\u00f6rger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol.\u00a02589. Springer, Heidelberg (2003)","DOI":"10.1007\/3-540-36498-6_21"},{"key":"4_CR37","unstructured":"Ober, I., Bozga, M.: Adapting and optimizing existing timed model checking tools to uml tools. Technical Report IST\/33522\/WP2.1\/D2.1.2, Verimag (December 2002)"},{"key":"4_CR38","unstructured":"OMG. OMG Unified Modeling Language Specification, Version 1.4 (September 2001)"},{"key":"4_CR39","series-title":"Lecture Notes in Computer Science","first-page":"430","volume-title":"\u00abUML\u00bb \u201999 - The Unified Modeling Language. Beyond the Standard","author":"I. Paltor","year":"1999","unstructured":"Paltor, I., Lilius, J.: Formalising uml state machines for model checking. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol.\u00a01723, pp. 430\u2013445. Springer, Heidelberg (1999)"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"Sch\u00e4fer, T., Knapp, A., Merz, S.: Model Checking UML State Machines and Collaborations. Electronic Notes in Theoretical Computer Science\u00a055(3) (2001)","DOI":"10.1016\/S1571-0661(04)00262-2"},{"key":"4_CR41","unstructured":"Shen, W., Compton, K., Huggins, J.K.: A toolset for supporting uml static and dynamic model checking. In: Feather and Goedicke [11], pp. 315\u2013318"},{"key":"4_CR42","unstructured":"Westphal, B.: Exploiting Object Symmetry in Verification of UML-Designs. Master\u2019s thesis, Carl von Ossietzky Universit\u00e4t Oldenburg (April 2001)"},{"key":"4_CR43","unstructured":"Xie, F., Levin, V., Browne, J.: Model Checking for an Executable Subset of UML. In: Feather and Goedicke [11]"},{"key":"4_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/3-540-45923-5_5","volume-title":"Fundamental Approaches to Software Engineering","author":"F. Xie","year":"2002","unstructured":"Xie, F., Browne, J.: Integrated State Space Reduction for Model Checking Executable Object-oriented Software System Designs. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol.\u00a02306, p. 64. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39656-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,30]],"date-time":"2021-10-30T06:04:29Z","timestamp":1635573869000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39656-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203032","9783540396567"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39656-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}