{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:17:01Z","timestamp":1775873821626,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642336652","type":"print"},{"value":"9783642336669","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33666-9_22","type":"book-chapter","created":{"date-parts":[[2012,9,18]],"date-time":"2012-09-18T16:50:20Z","timestamp":1347987020000},"page":"335-351","source":"Crossref","is-referenced-by-count":25,"title":["Assume-Guarantee Scenarios: Semantics and Synthesis"],"prefix":"10.1007","author":[{"given":"Shahar","family":"Maoz","sequence":"first","affiliation":[]},{"given":"Yaniv","family":"Sa\u2019ar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Alfonso, A., Braberman, V.A., Kicillof, N., Olivero, A.: Visual timed event scenarios. In: Finkelstein, A., Estublier, J., Rosenblum, D.S. (eds.) ICSE, pp. 168\u2013177. IEEE Computer Society (2004)","DOI":"10.1109\/ICSE.2004.1317439"},{"issue":"3","key":"22_CR2","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10515-007-0012-6","volume":"14","author":"M. Autili","year":"2007","unstructured":"Autili, M., Inverardi, P., Pelliccione, P.: Graphical scenarios for specifying temporal properties: an automated approach. Autom. Softw. Eng.\u00a014(3), 293\u2013340 (2007)","journal-title":"Autom. Softw. Eng."},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"2007","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: Time for Playing Games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 121\u2013125. Springer, Heidelberg (2007)"},{"issue":"3","key":"22_CR4","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R. Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. Journal of Computer and System Sciences\u00a078(3), 911\u2013938 (2012)","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"22_CR5","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(1), 45\u201380 (2001)","journal-title":"Formal Methods in System Design"},{"key":"22_CR6","unstructured":"Greenyer, J.: Scenario-based Design of Mechatronic Systems. PhD thesis, University of Paderborn, Department of Computer Science (2011)"},{"key":"22_CR7","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)"},{"issue":"2","key":"22_CR8","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s10270-007-0054-z","volume":"7","author":"D. Harel","year":"2008","unstructured":"Harel, D., Maoz, S.: Assert and negate revisited: Modal semantics for UML sequence diagrams. Software and Systems Modeling\u00a07(2), 237\u2013252 (2008)","journal-title":"Software and Systems Modeling"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Harel, D., Maoz, S., Szekely, S., Barkan, D.: PlayGo: towards a comprehensive tool for scenario based programming. In: ASE, pp. 359\u2013360. ACM (2010)","DOI":"10.1145\/1858996.1859075"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Harel, D., Marelly, R.: Come, Let\u2019s Play: Scenario-Based Programming Using LSC\u2019s and the Play-Engine. Springer (2003)","DOI":"10.1007\/978-3-642-19029-2"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Harel, D., Pnueli, A.: On the Development of Reactive Systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. ATO ASI Series, vol.\u00a0F-13, pp. 477\u2013498. Springer (1985)","DOI":"10.1007\/978-3-642-82453-1_17"},{"issue":"3","key":"22_CR12","doi-asserted-by":"publisher","first-page":"970","DOI":"10.1016\/j.jcss.2011.08.008","volume":"78","author":"D. Harel","year":"2012","unstructured":"Harel, D., Segall, I.: Synthesis from scenario-based specifications. Journal of Computer and System Sciences\u00a078(3), 970\u2013980 (2012)","journal-title":"Journal of Computer and System Sciences"},{"issue":"4","key":"22_CR13","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/s10270-005-0087-0","volume":"4","author":"\u00d8. Haugen","year":"2005","unstructured":"Haugen, \u00d8., Husa, K.E., Runde, R.K., St\u00f8len, K.: STAIRS towards formal design with sequence diagrams. Software and Systems Modeling\u00a04(4), 355\u2013367 (2005)","journal-title":"Software and Systems Modeling"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Jackson, M.: The world and the machine. In: Perry, D.E., Jeffrey, R., Notkin, D. (eds.) ICSE, pp. 283\u2013292. ACM (1995)","DOI":"10.1145\/225014.225041"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-540-69489-2_6","volume-title":"Models in Software Engineering","author":"A. Knapp","year":"2007","unstructured":"Knapp, A., Wuttke, J.: Model Checking of UML 2.0 Interactions. In: K\u00fchne, T. (ed.) MoDELS 2006. LNCS, vol.\u00a04364, pp. 42\u201351. Springer, Heidelberg (2007)"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"K\u00f6nighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications using simple counterstrategies. In: FMCAD, pp. 152\u2013159. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351127"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Kr\u00fcger, I., Grosu, R., Scholz, P., Broy, M.: From MSCs to Statecharts. In: DIPES, pp. 61\u201372 (1998)","DOI":"10.1007\/978-0-387-35570-2_5"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-642-00593-0_6","volume-title":"Fundamental Approaches to Software Engineering","author":"H. Kugler","year":"2009","unstructured":"Kugler, H., Plock, C., Pnueli, A.: Controller Synthesis from LSC Requirements. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 79\u201393. Springer, Heidelberg (2009)"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-00768-2_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Kugler","year":"2009","unstructured":"Kugler, H., Segall, I.: Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 77\u201391. Springer, Heidelberg (2009)"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-63166-6_7","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"1997","unstructured":"Kupferman, O., Vardi, M.Y.: Module Checking Revisited. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 36\u201347. Springer, Heidelberg (1997)"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The temporal logic of concurrent and reactive systems: specification. Springer (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Maoz, S., Harel, D.: From multi-modal scenarios to code: compiling LSCs into AspectJ. In: SIGSOFT FSE, pp. 219\u2013230. ACM (2006)","DOI":"10.1145\/1181775.1181802"},{"issue":"4","key":"22_CR23","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/2000799.2000804","volume":"20","author":"S. Maoz","year":"2011","unstructured":"Maoz, S., Harel, D., Kleinbort, A.: A compiler for multimodal scenarios: Transforming LSCs into AspectJ. ACM Trans. Softw. Eng. Methodol.\u00a020(4), 18 (2011)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Maoz, S., Sa\u2019ar, Y.: Counter play-out: Debugging unrealizable scenario-based specifications (in preparation, 2012)","DOI":"10.1109\/ICSE.2013.6606570"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A.: Faster solutions of Rabin and Streett games. In: LICS, pp. 275\u2013284. IEEE Computer Society (2006)","DOI":"10.1109\/LICS.2006.23"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of Reactive(1) Designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"22_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-14295-6_18","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2010","unstructured":"Pnueli, A., Sa\u2019ar, Y., Zuck, L.D.: Jtlv: A Framework for Developing Verification Algorithms. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 171\u2013174. Springer, Heidelberg (2010)"},{"issue":"1\/2","key":"22_CR29","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R.S. Streett","year":"1982","unstructured":"Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control\u00a054(1\/2), 121\u2013141 (1982)","journal-title":"Information and Control"},{"key":"22_CR30","doi-asserted-by":"crossref","unstructured":"Whittle, J., Schumann, J.: Generating statechart designs from scenarios. In: ICSE, pp. 314\u2013323. ACM (2000)","DOI":"10.1145\/337180.337217"}],"container-title":["Lecture Notes in Computer Science","Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33666-9_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:33:56Z","timestamp":1744158836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33666-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642336652","9783642336669"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33666-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}