{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:53:07Z","timestamp":1760586787594,"version":"3.41.0"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,1,16]],"date-time":"2016-01-16T00:00:00Z","timestamp":1452902400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Requirements Eng"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s00766-015-0242-2","type":"journal-article","created":{"date-parts":[[2016,1,16]],"date-time":"2016-01-16T09:54:38Z","timestamp":1452938078000},"page":"239-274","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Declaratively building behavior by means of scenario clauses"],"prefix":"10.1007","volume":"22","author":[{"given":"Fernando","family":"Asteasuain","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V\u00edctor","family":"Braberman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,16]]},"reference":[{"key":"242_CR1","doi-asserted-by":"publisher","unstructured":"Alfonso A, Braberman V, Kicillof N, Olivero A (2004) Visual timed event scenarios. In: 26th ICSE\u201904, pp 168\u2013177","DOI":"10.1109\/ICSE.2004.1317439"},{"key":"242_CR2","doi-asserted-by":"publisher","unstructured":"Areces C, Hoffmann G, Denis A (2010) Modal logics with counting. In: 17th workshop on logic, language, information and computation, Brazil. Springer, Berlin, Heidelberg, pp 98\u2013109","DOI":"10.1007\/978-3-642-13824-9_9"},{"key":"242_CR3","unstructured":"Asteasuain F, Braberman V (2010) Specification patterns can be formal and also easy. In: The 22nd international conference on software engineering and knowledge engineering (SEKE), pp 430\u2013436"},{"issue":"3","key":"242_CR4","first-page":"293","volume":"14","author":"M Autili","year":"2007","unstructured":"Autili M, Inverardi P, Pelliccione P (2007) Graphical scenarios for specifying temporal properties: an automated approach. ASE 14(3):293\u2013340","journal-title":"ASE"},{"key":"242_CR5","doi-asserted-by":"publisher","unstructured":"Autili M, Pelliccione P (2008) Towards a graphical tool for refining user to system requirements. In: Electronic notes in theoretical computer science (ENTCS), vol\u00a0211, pp 147\u2013157","DOI":"10.1016\/j.entcs.2008.04.037"},{"key":"242_CR6","doi-asserted-by":"publisher","unstructured":"Bianculli D, Ghezzi C, Pautasso C, Senti P (2012) Specification patterns from research to industry: a case study in service-based applications. In: Proceedings of the 2012 international conference on software engineering. IEEE Press, pp 968\u2013976","DOI":"10.1109\/ICSE.2012.6227125"},{"key":"242_CR7","unstructured":"Bloem R, Cavada R, Eisner C, Pill I, Roveri M, Semprini S (2004) Manual for property simulation and assurance tool (deliverable 1.2\/4\u20135). In: Technical report, PROSYD Project, Technical Report"},{"key":"242_CR8","doi-asserted-by":"publisher","unstructured":"Boker U, Chatterjee K, Henzinger TA, Kupferman O (2011) Temporal specifications with accumulative values. In: 26th annual IEEE symposium on logic in computer science (LICS), 2011. IEEE, pp 43\u201352","DOI":"10.1109\/LICS.2011.33"},{"key":"242_CR9","doi-asserted-by":"publisher","unstructured":"Bosscher D, Polak I, Vaandrager F (1994) Verification of an audio control protocol. In: Formal techniques in real-time and fault-tolerant systems. Springer, Berlin, Heidelberg,\u00a0pp 170\u2013192","DOI":"10.1007\/3-540-58468-4_165"},{"key":"242_CR10","doi-asserted-by":"publisher","unstructured":"Bouajjani A, Lakhnech Y, Yovine S (1996) Model checking for extended timed temporal logics. In: Formal techniques in real-time and fault-tolerant systems. Springer, Berlin, Heidelberg,\u00a0pp 306\u2013326","DOI":"10.1007\/3-540-61648-9_48"},{"key":"242_CR11","doi-asserted-by":"publisher","unstructured":"Braberman V, Garbervestky D, Kicillof N, Monteverde D, Olivero A (2009) Speeding up model checking of timed-models by combining scenario specialization and live component analysis. In: Formal modeling and analysis of timed systems. Springer, Berlin, Heidelberg,\u00a0pp 58\u201372","DOI":"10.1007\/978-3-642-04368-0_7"},{"issue":"12","key":"242_CR12","first-page":"1028","volume":"31","author":"V Braberman","year":"2005","unstructured":"Braberman V, Kicillof N, Olivero A (2005) A scenario-matching approach to the description and model checking of real-time properties. IEEE TSE 31(12):1028\u20131041","journal-title":"IEEE TSE"},{"key":"242_CR13","volume-title":"Model checking","author":"E Clarke","year":"1999","unstructured":"Clarke E, Grumberg O, Peled D (1999) Model checking. Springer, New York"},{"key":"242_CR14","unstructured":"\u201cBuchi online Store\u201d. In: http:\/\/buchi.im.ntu.edu.tw\/index.php\/browse\/index\/"},{"key":"242_CR15","doi-asserted-by":"publisher","unstructured":"Cobleigh R, Avrunin G, Clarke L (2006) User guidance for creating precise and accessible property specifications. In: Proceedings of the 14th ACM SIGSOFT international symposium on foundations of software engineering. ACM, p 218","DOI":"10.1145\/1181775.1181801"},{"key":"242_CR16","doi-asserted-by":"publisher","unstructured":"Dalal S, Jain A, Karunanithi N, Leaton J, Lott C, Patton G, Horowitz B (1999) Model-based testing in practice. In:\u00a0Proceedings of the 21st international conference on software engineering. ACM,\u00a0pp 285\u2013294","DOI":"10.1145\/302405.302640"},{"key":"242_CR17","unstructured":"David S, Orni A (2005) Property-by-example guide: a handbook of psl\/sugar examples-prosyd deliverable d1. 1\/3"},{"issue":"5","key":"242_CR18","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1145\/503271.503226","volume":"26","author":"L Alfaro De","year":"2001","unstructured":"De Alfaro L, Henzinger T (2001) Interface automata. ACM SIGSOFT Softw Eng Notes 26(5):120","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"issue":"2","key":"242_CR19","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/192218.192226","volume":"3","author":"L Dillon","year":"1994","unstructured":"Dillon L, Kutty G, Moser L, Melliar-Smith P, Ramakrishna Y (1994) A graphical interval logic for specifying concurrent systems. ACM Trans Softw Eng Methodol (TOSEM) 3(2):131\u2013165","journal-title":"ACM Trans Softw Eng Methodol (TOSEM)"},{"key":"242_CR20","doi-asserted-by":"publisher","unstructured":"D\u2019Ippolito N, Braberman V, Piterman N, Uchitel S (2010) Synthesis of live behaviour models. In: Proceedings of the 18th ACM SIGSOFT international symposium on foundations of software engineering. ACM SIGSOFT","DOI":"10.1145\/1882291.1882305"},{"key":"242_CR21","unstructured":"Dwyer M, Avrunin G, Corbett J \u201cSpecification Patterns Web Site\u201d. In: http:\/\/patterns.projects.cis.ksu.edu\/documentation\/patterns.shtml"},{"key":"242_CR22","doi-asserted-by":"publisher","unstructured":"Dwyer M, Avrunin G, Corbett J (1999) Patterns in property specifications for finite-state verification. In: Proceedings of the 21st international conference on software engineering ICSE, vol\u00a099","DOI":"10.1145\/302405.302672"},{"key":"242_CR23","volume-title":"A practical introduction to PSL (series on integrated circuits and systems)","author":"C Eisner","year":"2006","unstructured":"Eisner C, Fisman D (2006) A practical introduction to PSL (series on integrated circuits and systems). Springer, Secaucus"},{"key":"242_CR24","doi-asserted-by":"publisher","unstructured":"Fritz C, Wilke T (2002) State space reductions for alternating b\u00fcchi automata quotienting by simulation equivalences. In: FST TCS 2002: foundations of software technology and theoretical computer science. Springer, pp 157\u2013168","DOI":"10.1007\/3-540-36206-1_15"},{"key":"242_CR25","unstructured":"Gary MR, Johnson DS (1979) Computers and intractability: a guide to the theory of np-completeness.\u00a0W. H. Freeman and Company, San Francisco"},{"key":"242_CR26","doi-asserted-by":"publisher","unstructured":"Giannakopoulou D, Magee J (2003) Fluent model checking for event-based systems. In: Proceedings of the 9th European software engineering conference. ACM, p 266","DOI":"10.1145\/940071.940106"},{"key":"242_CR27","doi-asserted-by":"crossref","unstructured":"Harel D, Marelly R Playing with time: On the specification and execution of time-enriched lscs. In: MASCOTS\u00a0\u201902. IEEE computer society, pp 193\u2013202","DOI":"10.1109\/MASCOT.2002.1167077"},{"issue":"6","key":"242_CR28","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/605466.605479","volume":"27","author":"G Holzmann","year":"2002","unstructured":"Holzmann G (2002) The logic of bugs. ACM Softw Eng Notes 27(6):87","journal-title":"ACM Softw Eng Notes"},{"key":"242_CR29","unstructured":"IEEE-Commission et\u00a0al (2005) Ieee standard for property specification language (psl). Tech. rep., Technical report, IEEE, 2005. IEEE Std 1850-2005"},{"key":"242_CR30","unstructured":"Konrad S, Cheng B (2005) Real-time specification patterns. In: Proceedings of the 27th ICSE. ACM, pp 372\u2013381"},{"key":"242_CR31","doi-asserted-by":"publisher","unstructured":"Kupferman O, Piterman N, Vardi M (2001) Extended temporal logic revisited. In: CONCUR 2001 concurrency theory, pp 519\u2013535","DOI":"10.1007\/3-540-44685-0_35"},{"key":"242_CR32","unstructured":"Lamsweerde AV (2001) Goal-oriented requirements engineering: a guided tour. In: RE\u201901\u2014international joint conference on RE"},{"key":"242_CR33","doi-asserted-by":"crossref","unstructured":"Linn J (1993) RFC1508: generic security service application program interface RFC Editor United States","DOI":"10.17487\/rfc1508"},{"key":"242_CR34","volume-title":"Event processing for business: organizing the real-time enterprise","author":"D Luckham","year":"2011","unstructured":"Luckham D (2011) Event processing for business: organizing the real-time enterprise. Wiley, Hoboken"},{"key":"242_CR35","unstructured":"McCarthy J, Hayes P (1968) Some philosophical problems from the standpoint of artificial intelligence. Stanford University"},{"key":"242_CR36","unstructured":"[MS-NNS] (2008) NET NegotiateStream Protocol Specification v2.0. http:\/\/msdn.microsoft.com\/en-us\/library\/cc236723.aspx , July (2008)"},{"key":"242_CR37","unstructured":"Noda N, Kishi T (2006) An aspect-oriented modeling mechanism based on state diagrams. In: 9th international workshop on AOM"},{"issue":"3","key":"242_CR38","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1017\/S1471068406002973","volume":"7","author":"N Pelov","year":"2007","unstructured":"Pelov N, Denecker M, Bruynooghe M (2007) Well-founded and stable semantics of logic programs with aggregates. Theory Pract Logic Program 7(3):301","journal-title":"Theory Pract Logic Program"},{"key":"242_CR39","unstructured":"Piterman N, Pnueli A, Sa\u2019ar Y (2006) Synthesis of reactive (1) designs. In: Lecture notes in computer science, vol 3855, p 364"},{"key":"242_CR40","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, 1977. IEEE, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"242_CR41","doi-asserted-by":"crossref","unstructured":"Pnueli A (1986) Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. Current trends in Concurrency pp 510\u2013584","DOI":"10.1007\/BFb0027047"},{"key":"242_CR42","doi-asserted-by":"crossref","unstructured":"Post A, Hoenicke J (2012) Formalization and analysis of real-time requirements: a feasibility study at bosch. In: VSTTE, pp 225\u2013240","DOI":"10.1007\/978-3-642-27705-4_18"},{"issue":"1","key":"242_CR43","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/s00766-011-0145-9","volume":"17","author":"A Post","year":"2012","unstructured":"Post A, Menzel I, Hoenicke J, Podelski A (2012) Automotive behavioral requirements expressed in a specification pattern system: a case study at bosch. Requir Eng 17(1):19\u201333","journal-title":"Requir Eng"},{"key":"242_CR44","unstructured":"R, RW, Viggers K (2004) Implementing protocols via declarative event patterns. In: ACM sigsoft international symposium on FSE (FSE-12), pp 158\u2013169"},{"key":"242_CR45","doi-asserted-by":"publisher","unstructured":"S\u00e1nchez C, Leucker M (2010) Regular linear temporal logic with past. In: Verification, model checking, and abstract interpretation. Springer, pp 295\u2013311","DOI":"10.1007\/978-3-642-11319-2_22"},{"key":"242_CR46","doi-asserted-by":"publisher","unstructured":"Sengupta B, Cleaveland R (2002) Triggered message sequence charts. In: SIGSOFT FSE, pp 167\u2013176","DOI":"10.1145\/587051.587077"},{"key":"242_CR47","doi-asserted-by":"publisher","unstructured":"Sibay G, Uchitel S, Braberman V (2008) Existential live sequence charts revisited. In: Proceedings of ICSE. ACM New York, pp 41\u201350","DOI":"10.1145\/1368088.1368095"},{"key":"242_CR48","unstructured":"Smith M, Holzmann G, Etessami K (2001) Events and constraints: a graphical editor for capturing logic requirements of programs. In: Proceedings of fifth IEEE international symposium on requirements engineering, 2001. IEEE, pp 14\u201322"},{"key":"242_CR49","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/581339.581345","volume":"24","author":"R Smith","year":"2002","unstructured":"Smith R, Avrunin G, Clarke L, Osterweil L (2002) Propel: an approach supporting property elucidation. ICSE 24:11\u201321","journal-title":"ICSE"},{"key":"242_CR50","doi-asserted-by":"publisher","unstructured":"Somenzi F, Bloem R (2000) Efficient b\u00fcchi automata from ltl formulae. In: Computer aided verification. Springer, pp 248\u2013263","DOI":"10.1007\/10722167_21"},{"key":"242_CR51","doi-asserted-by":"publisher","unstructured":"Tsay Y, Chen Y, Tsai M, Wu K, Chan W (2007) Goal: A graphical tool for manipulating b\u00fcchi automata and temporal formulae. In: Tools and algorithms for the construction and analysis of systems, pp 466\u2013471","DOI":"10.1007\/978-3-540-71209-1_35"},{"key":"242_CR52","doi-asserted-by":"publisher","unstructured":"Tsay Y, Tsai M, Chang J, Chang Y (2011) B\u00fcchi store: an open repository of b\u00fcchi automata. In: Tools and algorithms for the construction and analysis of systems pp 262\u2013266","DOI":"10.1007\/978-3-642-19835-9_23"},{"key":"242_CR53","doi-asserted-by":"publisher","unstructured":"Uchitel S, Kramer J, Magee J (2002) Negative scenarios for implied scenario elicitation. In: Proceedings of FSE\u00a0\u201902. ACM Press, pp 109\u2013118","DOI":"10.1145\/587051.587069"},{"key":"242_CR54","volume-title":"Practical model-based testing: a tools approach","author":"M Utting","year":"2007","unstructured":"Utting M, Legeard B (2007) Practical model-based testing: a tools approach. Morgan Kaufmann, San Francisco"},{"key":"242_CR55","volume-title":"Handbook of knowledge representation","author":"F Harmelen Van","year":"2008","unstructured":"Van Harmelen F, Lifschitz V, Porter B (2008) Handbook of knowledge representation, vol 1. Elsevier Science, San Diego"},{"key":"242_CR56","doi-asserted-by":"crossref","unstructured":"Vardiy M, Wolperz P (1994) Reasoning about infinite computations","DOI":"10.1006\/inco.1994.1092"},{"key":"242_CR57","doi-asserted-by":"publisher","unstructured":"Veanes M, Schulte W (2008) Protocol modeling with model program composition. In: Lecture notes in computer science, vol 5048, p 324","DOI":"10.1007\/978-3-540-68855-6_21"},{"issue":"1\u20132","key":"242_CR58","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper P (1983) Temporal logic can be more expressive. Inf Control 56(1\u20132):72\u201399","journal-title":"Inf Control"},{"key":"242_CR59","doi-asserted-by":"publisher","unstructured":"Wolper P, Vardi M, Sistla A (1983) Reasoning about infinite computation paths. In: 24th annual symposium on foundations of computer science, 1983. IEEE, pp 185\u2013194","DOI":"10.1109\/SFCS.1983.51"},{"key":"242_CR60","doi-asserted-by":"publisher","unstructured":"Wu Z (2007) On the expressive power of qltl. In: Proceedings of the 4th international conference on theoretical aspects of computing. Springer, pp 467\u2013481","DOI":"10.1007\/978-3-540-75292-9_32"}],"container-title":["Requirements Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00766-015-0242-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00766-015-0242-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00766-015-0242-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00766-015-0242-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:32:47Z","timestamp":1748752367000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00766-015-0242-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,16]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["242"],"URL":"https:\/\/doi.org\/10.1007\/s00766-015-0242-2","relation":{},"ISSN":["0947-3602","1432-010X"],"issn-type":[{"type":"print","value":"0947-3602"},{"type":"electronic","value":"1432-010X"}],"subject":[],"published":{"date-parts":[[2016,1,16]]}}}