{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:00:17Z","timestamp":1725559217625},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540261896"},{"type":"electronic","value":"9783540320326"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11495628_2","type":"book-chapter","created":{"date-parts":[[2010,7,13]],"date-time":"2010-07-13T08:03:05Z","timestamp":1279008185000},"page":"26-42","source":"Crossref","is-referenced-by-count":12,"title":["Some Methodological Observations Resulting from Experience Using LSCs and the Play-In\/Play-Out Approach"],"prefix":"10.1007","author":[{"given":"David","family":"Harel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hillel","family":"Kugler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gera","family":"Weiss","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"2_CR1","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1023\/A:1025890110119","volume":"24","author":"D. Amyot","year":"2003","unstructured":"Amyot, D., Eberlein, A.: An Evaluation of Scenario Notations and Construction Approaches for Telecommunication Systems Development. Telecommunications Systems Journal\u00a024(1), 61\u201394 (2003)","journal-title":"Telecommunications Systems Journal"},{"issue":"2","key":"2_CR2","first-page":"70","volume":"17","author":"R. Alur","year":"1996","unstructured":"Alur, R., Holzmann, G.J., Peled, D.: An analyzer for message sequence charts. Software Concepts and Tools\u00a017(2), 70\u201377 (1996)","journal-title":"Software Concepts and Tools"},{"key":"2_CR3","unstructured":"Albert, S.: Cybernetix case-study: Informal description. Ametist web page (2002), \n                    \n                      http:\/\/ametist.cs.utwente.nl"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-48320-9_10","volume-title":"CONCUR\u201999. Concurrency Theory","author":"R. Alur","year":"1999","unstructured":"Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 114\u2013129. Springer, Heidelberg (1999)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-540-27755-2_2","volume-title":"Lectures on Concurrency and Petri Nets","author":"D. Barak","year":"2004","unstructured":"Barak, D., Harel, D., Marelly, R.: InterPlay: Horizontal Scale-Up and Transition to Design in Scenario-Based Programming. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol.\u00a03098, pp. 66\u201386. Springer, Heidelberg (2004)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc. Design Automation Conference 1995, DAC 1995 (1995)","DOI":"10.1145\/217474.217565"},{"key":"#cr-split#-2_CR8.1","doi-asserted-by":"crossref","unstructured":"Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design\u00a019(1), 45\u201380 (2001);","DOI":"10.1023\/A:1011227529550"},{"key":"#cr-split#-2_CR8.2","unstructured":"Preliminary version appeared in Proc. 3rd IFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS 1999)"},{"issue":"2","key":"2_CR9","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1023\/A:1011279932612","volume":"19","author":"W. Damm","year":"2001","unstructured":"Damm, W., Klose, J.: Verification of a radio-based signalling system using the statemate verification environment. Formal Methods in System Design\u00a019(2), 121\u2013141 (2001)","journal-title":"Formal Methods in System Design"},{"key":"2_CR10","unstructured":"Gilboa, A.: Finding All Super-Steps in LSC Specifications. Master\u2019s thesis, Weizmann Institute of Science, Israel (2003)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/3-540-45319-9_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.L. Gunter","year":"2001","unstructured":"Gunter, E.L., Muscholl, A., Peled, D.: Compositional message sequence charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 496\u2013511. Springer, Heidelberg (2001)"},{"key":"2_CR12","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 behavioral requirements. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 378\u2013398. Springer, Heidelberg (2002)"},{"key":"2_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19029-2","volume-title":"Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine","author":"D. Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)"},{"issue":"2","key":"2_CR14","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/s10270-002-0015-5","volume":"2","author":"D. Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Specifying and Executing Behavioral Requirements: The Play In\/Play-Out Approach. Software and System Modeling (SoSyM)\u00a02(2), 82\u2013107 (2003)","journal-title":"Software and System Modeling (SoSyM)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/3-540-45022-X_57","volume-title":"Automata, Languages and Programming","author":"J.G. Henriksen","year":"2000","unstructured":"Henriksen, J.G., Mukund, M., Kumar, K.N., Thiagarajan, P.S.: On message sequence graphs and finitely generated regular MSC languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 675\u2013686. Springer, Heidelberg (2000)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/3-540-44612-5_36","volume-title":"Mathematical Foundations of Computer Science 2000","author":"J.G. Henriksen","year":"2000","unstructured":"Henriksen, J.G., Mukund, M., Kumar, K.N., Thiagarajan, P.S.: Regular collections of Message Sequence Charts. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol.\u00a01893, pp. 675\u2013686. Springer, Heidelberg (2000)"},{"key":"2_CR17","unstructured":"Rhapsody. I-Logix, Inc., products web page, \n                    \n                      http:\/\/www.ilogix.com\/products\/"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-36481-1_2","volume-title":"Computational Methods in Systems Biology","author":"N. Kam","year":"2003","unstructured":"Kam, N., Harel, D., Kugler, H., Marelly, R., Pnueli, A., Hubbard, E.J.A., Stern, M.J.: Formal Modeling of C. elegans Development: A Scenario-Based Approach. In: Priami, C. (ed.) CMSB 2003. LNCS, vol.\u00a02602, pp. 4\u201320. Springer, Heidelberg (2003)"},{"key":"2_CR19","unstructured":"Kr\u00fcger, I.: Distributed System Design with Message Sequence Charts. PhD thesis, Department of Informatics, The Technical University of Munich (2000)"},{"key":"2_CR20","doi-asserted-by":"crossref","DOI":"10.1515\/9781400864041","volume-title":"Computer Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1995","unstructured":"Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1995)"},{"key":"2_CR21","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 chart. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 512. Springer, Heidelberg (2001)"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Lettrari, M., Klose, J.: Scenario-based monitoring and testing of real-time UML models. In: 4th Int. Conf. on the Unified Modeling Language, Toronto (October 2001)","DOI":"10.1007\/3-540-45441-1_24"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Marelly, R., Harel, D., Kugler, H.: Multiple instances and symbolic variables in executable sequence charts. In: Proc. 17th Ann. ACM Conf. on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2002), Seattle, WA, pp. 83\u2013100 (2002)","DOI":"10.1145\/582419.582429"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/BFb0053553","volume-title":"Foundations of Software Science and Computation Structures","author":"A. Muscholl","year":"1998","unstructured":"Muscholl, A., Peled, D., Su, Z.: Deciding properties for message sequence charts. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol.\u00a01378, pp. 226\u2013242. Springer, Heidelberg (1998)"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1007\/3-540-61604-7_83","volume-title":"CONCUR \u201996: Concurrency Theory","author":"S. Mauw","year":"1996","unstructured":"Mauw, S., Reniers, M.A.: Refinement in interworkings. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 671\u2013686. Springer, Heidelberg (1996)"},{"key":"2_CR26","unstructured":"UML. Documentation of the unified modeling language (UML). Available from the Object Management Group (OMG), \n                    \n                      http:\/\/www.omg.org"},{"key":"2_CR27","unstructured":"Z.120 ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS Geneva (1996)"}],"container-title":["Lecture Notes in Computer Science","Scenarios: Models, Transformations and Tools"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11495628_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T02:39:24Z","timestamp":1619491164000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11495628_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540261896","9783540320326"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/11495628_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}