{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:49:32Z","timestamp":1725572972625},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540374060"},{"type":"electronic","value":"9783540374114"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_22","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T05:07:51Z","timestamp":1154754471000},"page":"219-233","source":"Crossref","is-referenced-by-count":22,"title":["Check It Out: On the Efficient Formal Verification of Live Sequence Charts"],"prefix":"10.1007","author":[{"given":"Jochen","family":"Klose","sequence":"first","affiliation":[]},{"given":"Tobe","family":"Toben","sequence":"additional","affiliation":[]},{"given":"Bernd","family":"Westphal","sequence":"additional","affiliation":[]},{"given":"Hartmut","family":"Wittke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1023\/A:1011227529550","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, 45\u201380 (2001)","journal-title":"Formal Methods in System Design"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/11693017_18","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Westphal","year":"2006","unstructured":"Westphal, B., Toben, T.: The good, the bad and the ugly: Well-formedness of Live Sequence Charts. In: Baresi, L., Heckel, R. (eds.) FASE 2006 and ETAPS 2006. LNCS, vol.\u00a03922, pp. 230\u2013246. Springer, Heidelberg (2006)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","first-page":"33","volume-title":"SOFSEM 2006: Theory and Practice of Computer Science","author":"T. Toben","year":"2006","unstructured":"Toben, T., Westphal, B.: On the expressive power of LSCs. In: Wiedermann, J., Tel, G., Pokorn\u00fd, J., Bielikov\u00e1, M., \u0160tuller, J. (eds.) SOFSEM 2006. LNCS, vol.\u00a03831, pp. 33\u201343. Springer, Heidelberg (2006)"},{"key":"22_CR4","first-page":"133","volume-title":"Handbook of theor. comp. sc. (vol. B): Formal Models And Semantics","author":"W. Thomas","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of theor. comp. sc (vol. B): Formal Models And Semantics, pp. 133\u2013191. MIT Press, Cambridge (1990)"},{"key":"22_CR5","unstructured":"Klose, J.: Live Sequence Charts: A Graphical Formalism for the Specification of Communication Behavior. PhD thesis, C.v.O. Universit\u00e4t Oldenburg (2003)"},{"key":"22_CR6","unstructured":"Bohn, J., Damm, W., Wittke, H., Klose, J., Moik, A.: Modelling and validating train system applications using statemate and live sequence charts. In: Proc. IDPT 2002, Society for Design and Process Science (2002)"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Schinz, I., Toben, T., Mrugalla, C., Westphal, B.: The Rhapsody UML Verification Environment. In: Cuellar, J.R., Liu, Z. (eds.) Proc. SEFM 2004, pp. 174\u2013183 (2004)","DOI":"10.1109\/SEFM.2004.1347518"},{"key":"22_CR8","series-title":"ENTCS","first-page":"133","volume-title":"Proc. SoftMC 2005","author":"B. Westphal","year":"2005","unstructured":"Westphal, B.: LSC verification for UML models with unbounded creation and destruction. In: Cook, B., Scott Stoller, W.V. (eds.) Proc. SoftMC 2005. ENTCS, vol.\u00a0144:3, pp. 133\u2013145. Elsevier, Amsterdam (2005)"},{"key":"22_CR9","series-title":"ENTCS","first-page":"95","volume-title":"Proc. AVoCS 2005","author":"T. Toben","year":"2006","unstructured":"Toben, T., Westphal, B.: Concurrent LSC verification. In: Lazic, R. (ed.) Proc. AVoCS 2005. ENTCS, vol.\u00a0145, pp. 95\u2013111. Elsevier, Amsterdam (2006)"},{"issue":"4","key":"22_CR10","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/s10009-004-0145-x","volume":"7","author":"A. Bunker","year":"2004","unstructured":"Bunker, A., Gopalakrishnan, G., Slink, K.: Live sequence charts applied to hardware requirements specification and verification: A VCI bus interface model. Software Tools for Technology Transfer\u00a07(4), 341\u2013350 (2004)","journal-title":"Software Tools for Technology Transfer"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-36126-X_23","volume-title":"Formal Methods in Computer-Aided Design","author":"D. Harel","year":"2002","unstructured":"Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out of behvioral requirements. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 378\u2013398. Springer, Heidelberg (2002)"},{"key":"22_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19029-2","volume-title":"Come, Let\u2019s Play","author":"D. Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Come, Let\u2019s Play. Springer, Heidelberg (2003)"},{"key":"22_CR13","first-page":"529","volume-title":"ICECCS","author":"J. Sun","year":"2005","unstructured":"Sun, J., Dong, J.S.: Model checking Live Sequence Charts. In: ICECCS, pp. 529\u2013538. IEEE Computer Society, Los Alamitos (2005)"},{"key":"22_CR14","unstructured":"Gr\u00e9goire, B.: Automata oriented program verification. Master\u2019s thesis, Facult\u00e9s Universitaires Notre-Dame de la Paix, Namur (2002)"},{"key":"22_CR15","unstructured":"Wittke, H.: A Framework for Specification Verification for Complex Embedded Systems. PhD thesis, C.v.O. Universit\u00e4t Oldenburg (2005)"},{"key":"22_CR16","unstructured":"Schl\u00f6r, R.C.: Symbolic Timing Diagrams: A Visual Formalism for Model Verification. PhD thesis, C.v.O. Universit\u00e4t Oldenburg (2000)"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-540-31980-1_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Kugler","year":"2005","unstructured":"Kugler, H., et al.: Temporal logic for scenario-based specifications. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 445\u2013460. Springer, Heidelberg (2005)"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"494","DOI":"10.1007\/978-3-540-27863-4_27","volume-title":"SoftSpez","author":"M. Brill","year":"2004","unstructured":"Brill, M., et al.: Formal verification of LSCs in the development process. In: Ehrig, H., Damm, W., Desel, J., Gro\u00dfe-Rhode, M., Reif, W., Schnieder, E., Westk\u00e4mper, E. (eds.) INT 2004. LNCS, vol.\u00a03147, pp. 494\u2013516. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:30:01Z","timestamp":1619508601000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11817963_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}