{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T00:35:27Z","timestamp":1783384527747,"version":"3.54.6"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2007,8,4]],"date-time":"2007-08-04T00:00:00Z","timestamp":1186185600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2007,9,11]]},"DOI":"10.1007\/s10515-007-0012-6","type":"journal-article","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T14:13:46Z","timestamp":1186150426000},"page":"293-340","source":"Crossref","is-referenced-by-count":67,"title":["Graphical scenarios for specifying temporal properties: an automated approach"],"prefix":"10.1007","volume":"14","author":[{"given":"M.","family":"Autili","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"P.","family":"Inverardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"P.","family":"Pelliccione","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2007,8,4]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Alfonso, A., Braberman, V., Kicillof, N., Olivero, A.: Visual timed event scenarios. In: 26th ICSE\u201904. Edinburgh, Scotland, UK (2004)","DOI":"10.1109\/ICSE.2004.1317439"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, C., Peraldi-Frati, M.-A., Rigault, J.-P.: Scenario and property checking of real-time systems using a synchronous approach. In: 4th IEEE Int. Symp. on OO Real-Time Distributed Computing (2001)","DOI":"10.1109\/ISORC.2001.922869"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Autili, M., Inverardi, P., Pelliccione, P.: A scenario based notation for specifying temporal properties. In: 5th International Workshop on Scenarios and State Machines: Models, Algorithms and Tools (SCESM\u201906) Shanghai, China, May 27 (2006a)","DOI":"10.1145\/1138953.1138959"},{"key":"12_CR4","unstructured":"Autili, M., Pelliccione, P.: Towards a graphical tool for refining user to system requirements. In: 5th GT-VMT\u201906\u2013ETAPS\u201906, to appear in ENTCS (2006b)"},{"issue":"12","key":"12_CR5","doi-asserted-by":"crossref","first-page":"1028","DOI":"10.1109\/TSE.2005.131","volume":"31","author":"V. Braberman","year":"2005","unstructured":"Braberman, V., Kicillof, N., Olivero, A.: A scenario-matching approach to the description and model checking of real-time properties. IEEE Trans. Softw. Eng. 31(12), 1028\u20131041 (2005)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR6","unstructured":"Buchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. of the Int. Congress of Logic, Methodology and Philosophy of Science (1960)"},{"key":"12_CR7","unstructured":"Charmy Project: Charmy web site. http:\/\/www.di.univaq.it\/charmy (2004)"},{"key":"12_CR8","volume-title":"Model Checking","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Colangelo, D., Compare, D., Inverardi, P., Pelliccione, P.: Reducing software architecture models complexity: a slicing and abstraction approach. In: FORTE 2006, Paris, France, 26\u201329 September 2006, Lecture Notes in Computer Science, vol.\u00a04229, pp. 243\u2013258 (2006)","DOI":"10.1007\/11888116_19"},{"issue":"1","key":"12_CR10","doi-asserted-by":"crossref","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. Form. Methods Syst. Des. 19(1), 45\u201380 (2001)","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"12_CR11","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1145\/192218.192226","volume":"3","author":"L.K. Dillon","year":"1994","unstructured":"Dillon, L.K., Kutty, G., Moser, L.E., Melliar-Smith, P.M., Ramakrishna, Y.S.: A graphical interval logic for specifying concurrent systems. ACM Trans. Softw. Eng. Methodol. 3(2), 131\u2013165 (1994)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"12_CR13","volume-title":"Simple On-the-Fly Automatic Verification of Linear Temporal Logic, pp. 3\u201318","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple On-the-Fly Automatic Verification of Linear Temporal Logic, pp. 3\u201318. Chapman and Hall, London (1995)"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Harel, D., Marelly, R.: Playing with time: on the specification and execution of time-enriched LSCs. In: MASCOTS\u201902, p. 0193 (2002)","DOI":"10.1109\/MASCOT.2002.1167077"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Haugen, \u00d8, Comparing UML 2.0 interactions and MSC-2000. In: SAM, pp. 65\u201379 (2004)","DOI":"10.1007\/978-3-540-31810-1_5"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The logic of bugs. In: Proc. Foundations of Software Engineering (SIGSOFT 2002\/FSE-10) (2002)","DOI":"10.1145\/587051.587064"},{"key":"12_CR17","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison\u2013Wesley, Reading (2003)"},{"key":"12_CR18","unstructured":"ITU-T Recommendation Z. 120.: Message sequence charts. ITU Telecom. Standardisation Sector (1999)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Klose, J., Wittke, H.: An automata based interpretation of live sequence charts. In: TACAS 2001. Lecture Notes in Computer Science, vol.\u00a02031, pp. 512\u2013527 (2001)","DOI":"10.1007\/3-540-45319-9_35"},{"key":"12_CR20","volume-title":"11th Int. Conf. TACAS\u201905","author":"H. Kugler","year":"2005","unstructured":"Kugler, H., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y.: Temporal logic for scenario-based specifications. In: 11th Int. Conf. TACAS\u201905. Springer, Berlin (2005)"},{"key":"12_CR21","unstructured":"Lee, I., Sokolsky, O.: A graphical property specification language. In: High-Assurance Systems Engineering Workshop, Washington, DC (1997)"},{"key":"12_CR22","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1991)"},{"key":"12_CR23","unstructured":"Object Management Group (OMG): UML: superstructure version 2.0 (2004)"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symposium on Foundation of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"12_CR25","unstructured":"PSC Project: PSC web site. http:\/\/www.di.univaq.it\/psc2ba (2005)"},{"key":"12_CR26","unstructured":"Smith, M.H., Holzmann, G.J., Etessami, K.: Events and constraints: a graphical editor for capturing logic properties of programs. In: 5th International Symposium on Requirements Engineering, August 2001"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Smith, R.L., Avrunin, G.S., Clarke, L.A., Osterweil, L.J.: PROPEL: an approach supporting property elucidation. In: ICSE2002, pp. 11\u201321 (2002)","DOI":"10.1145\/581339.581345"},{"key":"12_CR28","unstructured":"St\u00f6rrle, H.: Semantics of interactions in UML 2.0. In: VLFM\u201903 Intl. Ws. Visual Languages and Formal Methods, at HCC\u201903, Auckland, NZ (2003)"},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Tivoli, M., Autili, M.: SYNTHESIS: a tool for synthesizing \u201ccorrect\u201d and protocol-enhanced adaptors. In: RSTI\u2013L\u2019objet Journal 12\/2006, WCAT\u201904, pp. 77\u2013103 (2004)","DOI":"10.3166\/objet.12.1.77-103"},{"issue":"1","key":"12_CR30","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/1005561.1005563","volume":"13","author":"S. Uchitel","year":"2004","unstructured":"Uchitel, S., Kramer, J., Magee, J.: Incremental elaboration of scenario-based specifications and behavior models using implied scenarios. ACM Trans. Softw. Eng. Methodol. 13(1), 37\u201385 (2004)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"12_CR31","unstructured":"Zanolin, L., Ghezzi, C., Baresi, L.: An approach to model and validate publish\/subscribe architectures. In: SAVCBS (2003)"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-007-0012-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-007-0012-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-007-0012-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T19:16:09Z","timestamp":1559157369000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-007-0012-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,8,4]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,9,11]]}},"alternative-id":["12"],"URL":"https:\/\/doi.org\/10.1007\/s10515-007-0012-6","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,8,4]]}}}