{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,17]],"date-time":"2023-08-17T14:42:06Z","timestamp":1692283326721},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,1,8]],"date-time":"2008-01-08T00:00:00Z","timestamp":1199750400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2008,5]]},"DOI":"10.1007\/s10270-007-0069-5","type":"journal-article","created":{"date-parts":[[2008,1,7]],"date-time":"2008-01-07T17:27:10Z","timestamp":1199726830000},"page":"157-175","source":"Crossref","is-referenced-by-count":12,"title":["Modeling and verification of a telecommunication application using live sequence charts and the Play-Engine tool"],"prefix":"10.1007","volume":"7","author":[{"given":"Pierre","family":"Combes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Harel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hillel","family":"Kugler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,1,8]]},"reference":[{"key":"69_CR1","volume-title":"Observers in the SCE and the SEE to Detect and Resolve Services Interactions","author":"I. Aggoun","year":"1997","unstructured":"Aggoun I. and Combes P. (1997). Observers in the SCE and the SEE to Detect and Resolve Services Interactions. IOS Press, Amsterdam"},{"key":"69_CR2","unstructured":"Altia Design & Altia FacePlate, web page http:\/\/www.altia.com"},{"issue":"2","key":"69_CR3","first-page":"70","volume":"17","author":"R. Alur","year":"1996","unstructured":"Alur R., Holzmann G. and Peled D. (1996). An analyzer for message sequence charts. Softw. Concepts Tools 17(2): 70\u201377","journal-title":"Softw. Concepts Tools"},{"issue":"1","key":"69_CR4","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1023\/A:1025890110119","volume":"24","author":"D. Amyot","year":"2003","unstructured":"Amyot D. and Eberlein A. (2003). An evaluation of scenario notations and construction approaches for telecommunication systems development. Telecommun. Syst. J. 24(1): 61\u201394","journal-title":"Telecommun. Syst. J."},{"key":"69_CR5","unstructured":"Bunker, A., Gopalakrishnan, G.: Verifying a VCI bus interface model using an LSC-based specification. In: Ehrig, H., Kramer, B.J., Ertas, A. (eds.) Proceedings of the 6th Biennial World Conference on Integrated Design and Process Technology, pp. 1\u201312 (2002)"},{"key":"69_CR6","unstructured":"Bunker, A., Slind, K.: Property generation for live sequence charts. Technical report, University of Utah (2003)"},{"key":"69_CR7","doi-asserted-by":"crossref","unstructured":"Castanet, R., Cavalli, A., Combes, P., Laurencot, P., MacKaya, M., Mederreg, A., Monin, W., Zaidi, F.: A multi-service and multi-protocol validation platform-experimentation results. In: TestCom, Lect. Notes in Comp. Sci., vol. 2978, pp. 17\u201332. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24704-3_2"},{"key":"69_CR8","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke E., Grumberg O. and Peled D. (1999). Model Checking. MIT Press, Cambridge"},{"key":"69_CR9","first-page":"1","volume-title":"SDL Forum, Lect. Notes in Comp. Sci., vol. 2708","author":"P. Combes","year":"2003","unstructured":"Combes P., Dubois F., Monin W. and Vincent D. (2003). Looking for better integration of design and performance engineering. In: Reed, R. (eds) SDL Forum, Lect. Notes in Comp. Sci., vol. 2708, pp 1\u201317. Springer, Heidelberg"},{"key":"69_CR10","unstructured":"Combes, P., Harel, D., Kugler, H.: Supplementary material on the depannage application. http:\/\/research.microsoft.com\/~hkugler\/Depannage\/"},{"key":"69_CR11","doi-asserted-by":"crossref","unstructured":"Combes, P., Harel, D., Kugler, H.: Modeling and Verification of a Telecommunication Application using Live Sequence Charts and the Play-Engine Tool. In: Proceedings of 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA \u201905), Lect. Notes in Comp. Sci., vol. 3707, pp. 414\u2013428. Springer, Heidelberg (2005)","DOI":"10.1007\/11562948_31"},{"key":"69_CR12","unstructured":"Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods Syst. Des. 19(1), 45\u201380 (2001). In: Preliminary version appeared in Proceedings of 3rd IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS\u201999)"},{"key":"69_CR13","doi-asserted-by":"crossref","unstructured":"Damm, W., Toben, T., Westphal, B.: On the expressive power of live sequence charts. In: Program Analysis and Compilation, Lect. Notes in Comp. Sci., vol. 4444, pp. 225\u2013246. Springer, Heidelberg (2006)","DOI":"10.1007\/978-3-540-71322-7_11"},{"issue":"1\u20133","key":"69_CR14","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/j.scico.2004.05.013","volume":"55","author":"W. Damm","year":"2005","unstructured":"Damm W. and Westphal B. (2005). Live and let die: LSC-based verification of UML-models. Sci. Comput. Program. 55(1\u20133): 117\u2013159","journal-title":"Sci. Comput. Program."},{"key":"69_CR15","unstructured":"e-SIM , web page http:\/\/www.e-sim.com\/home"},{"key":"69_CR16","unstructured":"Macromedia Flash, web page http:\/\/www.adobe.com\/products\/flash"},{"key":"69_CR17","doi-asserted-by":"crossref","unstructured":"Harel, D., Kugler, H.: Synthesizing state-based object systems from LSC specifications. Int. J. Found. Comput. Sci. (IJFCS) 13(1), 5\u201351 (2002). (Also, Proceedings of 5th International Conference on Implementation and Application of Automata (CIAA 2000), July 2000, Lecture Notes in Computer Science. Springer, Heidelberg, 2000)","DOI":"10.1142\/S0129054102000935"},{"key":"69_CR18","doi-asserted-by":"crossref","unstructured":"Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out of behavioral requirements. In: Proceedings of 4th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201902), Portland, Oregon, Lect. Notes in Comp. Sci., vol. 2517, pp. 378\u2013398 (2002). Also available as Tech. Report MCS02-08, The Weizmann Institute of Science","DOI":"10.1007\/3-540-36126-X_23"},{"key":"69_CR19","doi-asserted-by":"crossref","unstructured":"Harel, D., Kugler, H., Pnueli, A.: Smart play-out extended: time and forbidden elements. In: International Conference on Quality Software (QSIC04), pp. 2\u201310. IEEE Press, New York (2004)","DOI":"10.1109\/QSIC.2004.1357938"},{"key":"69_CR20","doi-asserted-by":"crossref","unstructured":"Harel, D., Kugler, H., Pnueli, A.: Synthesis revisited: generating statechart models from scenarios-based requirements. In: Formal Methods in Software and System Modeling, Lect. Notes in Comp. Sci., vol. 3393, pp. 309\u2013324. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-540-31847-7_18"},{"key":"69_CR21","doi-asserted-by":"crossref","unstructured":"Harel, D., Kugler, H., Weiss, G.: Some methodological observations resulting from experience using LSCs and the play-in\/play-out approach. In: Proceedings of scenarios: models, algorithms and tools, Lect. Notes in Comp. Sci., vol. 3466, pp. 26\u201342. Springer, Heidelberg (2005)","DOI":"10.1007\/11495628_2"},{"key":"69_CR22","doi-asserted-by":"crossref","unstructured":"Harel, D., Maoz, S.: Assert and negate revisited: modal semantics for UML sequence diagrams. Softw. Syst. Model. (SoSyM) (2007) (to appear). In: Early version in 5th International Workshop on Scenarios and State Machines: Models, Algorithms and Tools (SCESM\u201906)","DOI":"10.1145\/1138953.1138958"},{"key":"69_CR23","doi-asserted-by":"crossref","unstructured":"Harel, D., Marelly, R.: Playing with time: on the specification and execution of time-enriched LSCs. In: Proceedings of 10th IEEE\/ACM International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS\u201902). Fort Worth, Texas (2002)","DOI":"10.1109\/MASCOT.2002.1167077"},{"key":"69_CR24","doi-asserted-by":"crossref","unstructured":"Harel, D.,Marelly,R.: Come,Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, (2003)","DOI":"10.1007\/978-3-642-19029-2"},{"issue":"2","key":"69_CR25","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/s10270-002-0015-5","volume":"2","author":"D. Harel","year":"2003","unstructured":"Harel D. and Marelly R. (2003). Specifying and executing behavioral requirements: the play in\/play-out approach. Softw. Syst. Model. (SoSyM) 2(2): 82\u2013107","journal-title":"Softw. Syst. Model. (SoSyM)"},{"key":"69_CR26","unstructured":"Harel, D., Thiagarajan, P.: Message sequence charts. In: UML for Real: Design of Embedded Real-time Systems (2003)"},{"issue":"7","key":"69_CR27","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1002\/spe.4380240704","volume":"24","author":"K. Koskimies","year":"1994","unstructured":"Koskimies K. and Makinen E. (1994). Automatic synthesis of state machines from trace diagrams. Softwa. Practice Exp. 24(7): 643\u2013658","journal-title":"Softwa. Practice Exp."},{"key":"69_CR28","unstructured":"Koskimies, K., Mannisto, T., Systa, T., Tuomi, J.: SCED: a tool for dynamic modeling of object systems. Technical Report A-1996-4, University of Tampere (1996)"},{"key":"69_CR29","doi-asserted-by":"crossref","unstructured":"Kr\u00fcger, I., Grosu, R., Scholz, P., Broy, M.: From MSCs to statecharts. In: Proceedings of International Workshop on Distributed and Parallel Embedded Systems (DIPES\u201998), pp. 61\u201371. Kluwer, Dordrecht (1999)","DOI":"10.1007\/978-0-387-35570-2_5"},{"key":"69_CR30","doi-asserted-by":"crossref","unstructured":"Kugler, H., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y.: Temporal logic for scenario-based specifications. In: Halbwachs, N., Zuck, L.D. (eds.) Proceedings 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201905), Lect. Notes in Comp. Sci., vol. 3440, pp. 445\u2013460. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-540-31980-1_29"},{"key":"69_CR31","unstructured":"Leue, S., Mehrmann, L., Rezai, M.: Synthesizing ROOM models from message sequence chart specifications. Technical Report 98-06, University of Waterloo (1998)"},{"key":"69_CR32","volume-title":"Feature Interactions in Telecommunications and Software Systems VII","author":"L. Logrippo","year":"2003","unstructured":"Logrippo L. and Amyot D. (2003). Feature Interactions in Telecommunications and Software Systems VII. IOS Press, Amsterdam"},{"key":"69_CR33","doi-asserted-by":"crossref","unstructured":"Marelly, R., Harel, D., Kugler, H.: Multiple instances and symbolic variables in executable sequence charts. In: Proceedings of 17th Annual ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA\u201902), pp. 83\u2013100. Seattle, WA (2002)","DOI":"10.1145\/582419.582429"},{"key":"69_CR34","unstructured":"ITU-TS Recommendation Z.120 (11\/99): MSC 2000. ITU-TS, Geneva (1999)"},{"key":"69_CR35","unstructured":"OMEGA\u2014Correct development of real-time embedded systems. http:\/\/www-omega.imag.fr\/"},{"key":"69_CR36","volume-title":"Feature Interactions in Telecommunications and Software Systems VIII","author":"S. Reiff-Marganiec","year":"2005","unstructured":"Reiff-Marganiec S. (2005). Feature Interactions in Telecommunications and Software Systems VIII. IOS Press, Amsterdam"},{"key":"69_CR37","doi-asserted-by":"crossref","unstructured":"Schinz, I., Toben, T., Westphal, B.: The Rhapsody UML Verification Environment. In: 2nd International Conference on Software Engineering and Formal Methods. IEEE Computer Society Press, New York (2004)","DOI":"10.1109\/SEFM.2004.1347518"},{"key":"69_CR38","doi-asserted-by":"crossref","unstructured":"Sengupta, B., Cleaveland, R.: Triggered message sequence charts. In: Proceedings of the 10th ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 167\u2013176. ACM Press, New York (2002)","DOI":"10.1145\/587051.587077"},{"issue":"1","key":"69_CR39","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/1005561.1005563","volume":"13","author":"S. Uchitel","year":"2004","unstructured":"Uchitel S., Kramer J. and Magee J. (2004). Incremental elaboration of scenario-based specifications and behavior models using implied scenarios. ACM Trans. Softw. Eng. Methods 13(1): 37\u201385","journal-title":"ACM Trans. Softw. Eng. Methods"},{"key":"69_CR40","unstructured":"UML: Documentation of the unified modeling language (UML) (2007). Available from the Object Management Group (OMG), http:\/\/www.omg.org"},{"key":"69_CR41","doi-asserted-by":"crossref","unstructured":"Wang, T., Roychoudhury, A., Yap, R., Choudhary, S.: Symbolic execution of behavioral requirements. In: Jayaraman, B. (ed.) 6th International Symposium on Practical Aspects of Declarative Languages, (PADL 2004), Lect. Notes in Comp. Sci., vol. 3057, pp. 178\u2013192. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24836-1_13"},{"key":"69_CR42","doi-asserted-by":"crossref","unstructured":"Whittle, J., Saboo, J., Kwan, R.: From scenarios to code: an air traffic control case study. In: 25th International Conference on Software Engineering (ICSE 2003), pp. 490\u2013495. IEEE Computer Society, New York (2003)","DOI":"10.1109\/ICSE.2003.1201227"},{"key":"69_CR43","doi-asserted-by":"crossref","unstructured":"Whittle, J., Schumann, J.: Generating statechart designs from scenarios. In: 22nd International Conference on Software Engineering (ICSE 2000), pp. 314\u2013323. ACM Press, New York (2000)","DOI":"10.1145\/337180.337217"},{"key":"69_CR44","unstructured":"Z.120 ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva (1996)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-007-0069-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-007-0069-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-007-0069-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T11:55:24Z","timestamp":1559130924000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-007-0069-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,8]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,5]]}},"alternative-id":["69"],"URL":"https:\/\/doi.org\/10.1007\/s10270-007-0069-5","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1,8]]}}}