{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:46:47Z","timestamp":1725540407824},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_43","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"676-691","source":"Crossref","is-referenced-by-count":1,"title":["Verifying Real-Time Systems against Scenario-Based Requirements"],"prefix":"10.1007","author":[{"given":"Kim G.","family":"Larsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuhao","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brian","family":"Nielsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saulius","family":"Pusinskas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"43_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. TCS\u00a0126, 183\u2013235 (1994)","journal-title":"TCS"},{"issue":"2","key":"43_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":"43_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol.\u00a03185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"key":"43_CR4","series-title":"Lecture Notes in Computer Science","first-page":"87","volume-title":"Lectures on Concurrency and Petri Nets","author":"J. Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol.\u00a03098, pp. 87\u2013124. Springer, Heidelberg (2004)"},{"key":"43_CR5","doi-asserted-by":"crossref","unstructured":"Bontemps, Y.: Relating Inter-Agent and Intra-Agent Specifications: The Case of Live Sequence Charts. PhD thesis, University of Namur (2005)","DOI":"10.1007\/978-3-540-31982-5_23"},{"issue":"2","key":"43_CR6","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1016\/j.jal.2005.12.013","volume":"5","author":"Y. Bontemps","year":"2007","unstructured":"Bontemps, Y., Schobbens, P.-Y.: The computational complexity of scenario-based agent verification and design. J. Applied Logic\u00a05(2), 252\u2013276 (2007)","journal-title":"J. Applied Logic"},{"issue":"1","key":"43_CR7","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":"43_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-540-71322-7_11","volume-title":"Program Analysis and Compilation, Theory and Practice","author":"W. Damm","year":"2007","unstructured":"Damm, W., Toben, T., Westphal, B.: On the Expressive Power of Live Sequence Charts. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Wilhelm Festschrift. LNCS, vol.\u00a04444, pp. 225\u2013246. Springer, Heidelberg (2007)"},{"key":"43_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/3-540-46852-8_45","volume-title":"\u00abUML\u00bb \u201999 - The Unified Modeling Language. Beyond the Standard","author":"T. Firley","year":"1999","unstructured":"Firley, T., Huhn, M., Diethers, K., Gehrke, T., Goltz, U.: Timed Sequence Diagrams and Tool-Based Analysis - A Case Study. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol.\u00a01723, pp. 645\u2013660. Springer, Heidelberg (1999)"},{"key":"43_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/978-3-540-24727-2_15","volume-title":"Foundations of Software Science and Computation Structures","author":"B. Genest","year":"2004","unstructured":"Genest, B., Minea, M., Muscholl, A., Peled, D.: Specifying and Verifying Partial Order Properties Using Template MSCs. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 195\u2013210. Springer, Heidelberg (2004)"},{"key":"43_CR11","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":"1","key":"43_CR12","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1142\/S0129054102000935","volume":"13","author":"D. Harel","year":"2002","unstructured":"Harel, D., Kugler, H.: Synthesizing State-Based Object Systems from LSC Specifications. Int. J. of Foundations of Computer Science\u00a013(1), 5\u201351 (2002)","journal-title":"Int. J. of Foundations of Computer Science"},{"key":"43_CR13","unstructured":"ITU: Z. 120 ITU-TS Recommendation Z.120: Message Sequence Chart 2000 (1999)"},{"key":"43_CR14","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 Charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 512\u2013527. Springer, Heidelberg (2001)"},{"key":"43_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y.: 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":"43_CR16","unstructured":"Lahtinen, J.: Model checking timed safety instrumented systems. Research Report TKK-ICS-R3, Helsinki University of Technology, Espoo, Finland (2008)"},{"key":"43_CR17","unstructured":"Pusinskas, S.: From Live Sequence Charts to Uppaal. PhD thesis (forthcoming)"},{"key":"43_CR18","unstructured":"Rye-Andersen, J.G., Jensen, M.W., Goettler, R., Jakobsen, M.: PEEL: Property Extraction Engine for LSCs. Master thesis, Aalborg University (2004)"},{"key":"43_CR19","doi-asserted-by":"crossref","unstructured":"Sengupta, B., Cleaveland, R.: Triggered Message Sequence Charts. In: FSE (2002)","DOI":"10.1145\/587051.587077"},{"issue":"1\/2","key":"43_CR20","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: Kronos: A verification tool for real-time systems. STTT\u00a01(1\/2), 123\u2013133 (1997)","journal-title":"STTT"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:39Z","timestamp":1606186059000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}