{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:07Z","timestamp":1760202607833},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001164"},{"type":"electronic","value":"9783540361268"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36126-x_23","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:55:19Z","timestamp":1269899719000},"page":"378-398","source":"Crossref","is-referenced-by-count":64,"title":["Smart Play-out of Behavioral Requirements"],"prefix":"10.1007","author":[{"given":"David","family":"Harel","sequence":"first","affiliation":[]},{"given":"Hillel","family":"Kugler","sequence":"additional","affiliation":[]},{"given":"Rami","family":"Marelly","sequence":"additional","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable concurrent program specifications. In Proc. 16th Int. Colloq. Aut. Lang. Prog., volume 372 of Lect. Notes in Comp. Sci., pages 1\u201317. Springer-Verlag, 1989.","DOI":"10.1007\/BFb0035748"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, K. Etessami, and M. Yannakakis. Inference of message sequence charts. In Proc. 22nd Int. Conf. on Software Engineering (ICSE\u201900), Limerick, Ireland, June 2000.","DOI":"10.1145\/337180.337215"},{"issue":"2","key":"23_CR3","first-page":"70","volume":"17","author":"R. Alur","year":"1996","unstructured":"R. Alur, G.J. Holzmann, and D. Peled. An analyzer for message sequence charts. Software Concepts and Tools, 17(2):70\u201377, 1996.","journal-title":"Software Concepts and Tools"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur and M. Yannakakis. Model checking of message sequence charts. In Proc. 10th Int. Conf. on Concurrency Theory (CONCUR\u201999), Eindhoven, Netherlands, August 1999.","DOI":"10.1007\/3-540-48320-9_10"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"R. Bharadwaj and C. Heitmeyer. Model Checking Complete Requirements Specifications Using Abstraction. Automated Software Engineering, 6(1):37\u201368, January 1999.","DOI":"10.1023\/A:1008697817793"},{"issue":"2","key":"23_CR6","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2): 142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"W. Damm and D. Harel. LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design, 19(1), 2001. (Preliminary version in Proc. 3rdIFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS\u201999), (P. Ciancarini, A. Fantechi and R. Gorrieri, eds.), Kluwer Academic Publishers, 1999, pp. 293\u2013312.).","DOI":"10.1007\/978-0-387-35562-7_23"},{"issue":"2","key":"23_CR8","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1023\/A:1011279932612","volume":"19","author":"W. Damm","year":"2001","unstructured":"W. Damm and J. Klose. Verification of a Radio-based Signalling System using the STATE-MATE Verification Environment. Formal Methods in System Design, 19(2):121\u2013141, 2001.","journal-title":"Formal Methods in System Design"},{"key":"23_CR9","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"E.A. Emerson and E.M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241\u2013266, 1982.","journal-title":"Science of Computer Programming"},{"key":"23_CR10","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0096-0551(01)00017-0","volume":"27","author":"M. Fr\u00e4nzle","year":"2001","unstructured":"M. Fr\u00e4nzle and K. L\u00fcth. Visual Temporal Logic as a Rapid Prototyping Tool. Computer Languages, 27:93\u2013113, 2001.","journal-title":"Computer Languages"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Elsa L. Gunter, Anca Muscholl, and Doron Peled. Compositional message sequence charts. In Tools and Algorithms for Construction and Analysis of Systems, pages 496\u2013511, 2001.","DOI":"10.1007\/3-540-45319-9_34"},{"key":"23_CR12","series-title":"Lect Notes Comput Sci","first-page":"53","volume-title":"IEEE Computer","author":"D. Harel","year":"2001","unstructured":"D. Harel. From Play-In Scenarios To Code: An Achievable Dream. IEEE Computer, 34(1):53\u201360, January 2001. (Also in Fundamental Approaches to Software Engineering (FASE), Lecture Notes in Computer Science, Vol. 1783 (Tom Maibaum, ed.), Springer-Verlag, March 2000, pp. 22\u201334.)."},{"key":"23_CR13","series-title":"Lect Notes Comput Sci","first-page":"5","volume-title":"Int. J. of Foundations of Computer Science (IJFCS)","author":"D. Harel","year":"2002","unstructured":"D. Harel and H. Kugler. Synthesizing State-Based Object Systems from LSC Specifications. Int. J. of Foundations of Computer Science (IJFCS)., 13(1):5\u201351, Febuary 2002. (Also, Proc. Fifth Int. Conf. on Implementation and Application of Automata (CIAA 2000), July 2000, Lecture Notes in Computer Science, Springer-Verlag, 2000.)."},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"D. Harel and R. Marelly. Specifying and Executing Behavioral Requirements: The Play-In\/ Play-Out Approach. Tech. Report MCS01-15, The Weizmann Institute of Science, 2001.","DOI":"10.1145\/985072.985115"},{"key":"23_CR15","unstructured":"D. Harel and R. Marelly. Playing with Time: On the Specification and Execution of Time-Enriched LSCs. In Proc. 10th IEEE\/ACM International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS\u201902), Fort Worth, Texas, 2002. To appear."},{"key":"23_CR16","unstructured":"D. Harel and M. Politi. Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, 1998."},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"C. Heitmeyer, J. Kirby, B. Labaw, and R. Bharadwaj. SCR*: A Toolset for Specifying and Analyzing Software Requirements. In A.J. Hu and M.Y. Vardi, editors, Proc. 10th Intl. Conference on Computer Aided Verification (CAV\u201998), volume 1427 ofLect. Notes in Comp. Sci., Springer-Verlag, pages 5\u201351, 1998.","DOI":"10.21236\/ADA465334"},{"key":"23_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45022-X_57","volume-title":"Proceedings of the 27th International Colloquium on Automata Languages and Programming (ICALP\u20192000)","author":"J.G. Henriksen","year":"2000","unstructured":"J.G. Henriksen, M. Mukund, K. Narayan Kumar, and P.S. Thiagarajan. On Message Sequence Graphs and finitely generated regular MSC languages. In Proceedings of the 27th International Colloquium on Automata Languages and Programming (ICALP\u20192000), number 1853 in Lecture Notes in Computer Science, Geneva, Switzerland, 2000. Springer."},{"key":"23_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science (MFCS\u20192000)","author":"J.G. Henriksen","year":"2000","unstructured":"J.G. Henriksen, M. Mukund, K. Narayan Kumar, and P.S. Thiagarajan. Regular collections of Message Sequence Charts. In Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science (MFCS\u20192000), number 1893 in Lecture Notes in Computer Science, Bratislava, Slovakia, 2000. Springer-Verlag."},{"key":"23_CR20","unstructured":"I-logix,inc., products web page. http:\/\/www.ilogix.com\/fsprod.htm ."},{"key":"23_CR21","unstructured":"ITU. ITU-T recommendation Z.120: Message sequence chart (MSC)."},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"J. Klose and H. Wittke. An automata based interpretation of live sequence chart. In Proc. 7 th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901), 2001.","DOI":"10.1007\/3-540-45319-9_35"},{"issue":"1","key":"23_CR23","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1109\/52.646888","volume":"15","author":"K. Koskimies","year":"1988","unstructured":"K. Koskimies, T. Systa, J. Tuomi, and T. Mannisto. Automated support for modeling OO software. IEEE Software, 15(1):87\u201394, 1988.","journal-title":"IEEE Software"},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"I. Kruger, R. Grosu, P. Scholz, and M. Broy. From MSCs to statecharts. In Proc. DIPES\u201998. Kluwer, 1999.","DOI":"10.1007\/978-0-387-35570-2_5"},{"key":"23_CR25","unstructured":"O. Kupferman and M.Y. Vardi. Synthesis with incomplete information. In 2nd International Conference on Temporal Logic, pages 91\u2013106, Manchester, July 1997."},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"M. Lettrari and J. Klose. Scenario-based monitoring and testing of real-time uml models. In Proc. 4th Int. Conf. on the Unified Modeling Language, 2001.","DOI":"10.1007\/3-540-45441-1_24"},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"R. Marelly, D. Harel, and H. Kugler. Multiple Instances and Symbolic Variables in Executable Sequence Charts. In Proc. 17th Ann. ACM Conf. on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA\u201902), Seattle, WA, 2002. To appear. Also available as Tech. Report MCS02-05, Weizmann Institute of Science, 2002.","DOI":"10.1145\/582427.582429"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Anca Muscholl, Doron Peled, and Zhendong Su. Deciding properties for message sequence charts. In Foundations of Software Science and Computation Structure, pages 226\u2013242, 1998.","DOI":"10.1007\/BFb0053553"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symp. Princ. of Prog. Lang., pages 179\u2013190, 1989.","DOI":"10.1145\/75277.75293"},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In In R. Alurand T. Henzinger, editors, Proc. 8 th Intl. Conference on Computer Aided Verification (CAV\u201996), volume 1102 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 184\u2013195, 1996.","DOI":"10.1007\/3-540-61474-5_68"},{"key":"23_CR31","unstructured":"Rational,inc., web page. http:\/\/www.rational.com ."},{"key":"23_CR32","volume-title":"Real-Time Object-Oriented Modeling","author":"B. Selic","year":"1994","unstructured":"B. Selic, G. Gullekson, and P. Ward. Real-Time Object-Oriented Modeling. John Wiley & Sons, New York, 1994."},{"key":"23_CR33","unstructured":"UML. Documentation of the unified modeling language (UML). Available from the Object Management Group (OMG), http:\/\/www.omg.org ."},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"J. Whittle and J. Schumann. Generating statechart designs from scenarios. In Proc. 22nd Int. Conf. on Software Engineering (ICSE\u201900), Limerick, Ireland, June 2000.","DOI":"10.1145\/337180.337217"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36126-X_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,31]],"date-time":"2023-05-31T10:52:12Z","timestamp":1685530332000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36126-X_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001164","9783540361268"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-36126-x_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}