{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T13:18:57Z","timestamp":1715606337709},"reference-count":78,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,10,25]],"date-time":"2012-10-25T00:00:00Z","timestamp":1351123200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Comput Sci Res Dev"],"published-print":{"date-parts":[[2013,11]]},"DOI":"10.1007\/s00450-012-0233-1","type":"journal-article","created":{"date-parts":[[2012,10,24]],"date-time":"2012-10-24T11:59:18Z","timestamp":1351079958000},"page":"279-293","source":"Crossref","is-referenced-by-count":11,"title":["Supporting incremental behaviour model elaboration"],"prefix":"10.1007","volume":"28","author":[{"given":"Sebastian","family":"Uchitel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dalal","family":"Alrajeh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shoham","family":"Ben-David","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor","family":"Braberman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guido","family":"De Caso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"D\u2019Ippolito","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dario","family":"Fischbein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Diego","family":"Garbervetsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeff","family":"Kramer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandra","family":"Russo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"German","family":"Sibay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,10,25]]},"reference":[{"key":"233_CR1","volume-title":"Scenarios, stories, use cases: through the systems development life-cycle","author":"I Alexander","year":"2004","unstructured":"Alexander\u00a0I, Maiden\u00a0N (2004) Scenarios, stories, use cases: through the systems development life-cycle. Wiley, New York"},{"key":"233_CR2","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-78743-3_1","volume-title":"FASE","author":"D Alrajeh","year":"2008","unstructured":"Alrajeh\u00a0D, Russo\u00a0A, Uchitel\u00a0S (2008) Deriving non-zeno behavior models from goal models using ilp. In: Fiadeiro JL, Inverardi\u00a0P (eds) FASE. Lecture notes in computer science, vol 4961. Springer, Berlin, pp 1\u201315"},{"key":"233_CR3","first-page":"265","volume-title":"Proc of 31st intl conf on softw eng","author":"D Alrajeh","year":"2009","unstructured":"Alrajeh\u00a0D, Kramer\u00a0J, Russo\u00a0A, Uchitel\u00a0S (2009) Learning operational requirements from goal models. In: Proc of 31st intl conf on softw eng, pp 265\u2013275"},{"issue":"3","key":"233_CR4","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/j.jal.2008.10.002","volume":"7","author":"D Alrajeh","year":"2009","unstructured":"Alrajeh\u00a0D, Ray\u00a0O, Russo\u00a0A, Uchitel\u00a0S (2009) Using abduction and induction for operational requirements elaboration. J Appl Log 7(3):275\u2013288","journal-title":"J Appl Log"},{"issue":"3\u20134","key":"233_CR5","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/s00165-009-0128-5","volume":"22","author":"D Alrajeh","year":"2010","unstructured":"Alrajeh\u00a0D, Kramer\u00a0J, Russo\u00a0A, Uchitel\u00a0S (2010) Deriving non-zeno behaviour models from goal models using ilp. Form Asp Comput 22(3\u20134):217\u2013241","journal-title":"Form Asp Comput"},{"key":"233_CR6","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/978-3-642-28872-2_26","volume-title":"FASE","author":"D Alrajeh","year":"2012","unstructured":"Alrajeh\u00a0D, Kramer\u00a0J, Russo\u00a0A, Uchitel\u00a0S (2012) Learning from vacuously satisfiable scenario-based specifications. In: de Lara\u00a0J, Zisman\u00a0A (eds) FASE. Lecture notes in computer science, vol 7212. Springer, Berlin, pp 377\u2013393"},{"key":"233_CR7","volume-title":"Proc of 34th intl conf on softw eng","author":"D Alrajeh","year":"2012","unstructured":"Alrajeh\u00a0D, Kramer\u00a0J, van Lamsweerde\u00a0A, Russo\u00a0A, Uchitel\u00a0S (2012) Generating obstacle conditions for requirements completeness. In: Proc of 34th intl conf on softw eng"},{"issue":"1","key":"233_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/963927.963928","volume":"5","author":"R Alur","year":"2004","unstructured":"Alur\u00a0R, La Torre\u00a0S (2004) Deterministic generators and games for LTL fragments. ACM Trans Comput Log 5(1):1\u201325","journal-title":"ACM Trans Comput Log"},{"key":"233_CR9","volume-title":"Proceedings of the IFAC symposium on system structure and control","author":"E Asarin","year":"1998","unstructured":"Asarin\u00a0E, Maler\u00a0O, Pnueli\u00a0A, Sifakis\u00a0J (1998) Controller synthesis for timed automata. In: Proceedings of the IFAC symposium on system structure and control"},{"key":"233_CR10","first-page":"79","volume-title":"SAVCBS 2004 specification and verification of component-based systems","author":"M Autili","year":"2004","unstructured":"Autili\u00a0M, Inverardi\u00a0P, Tivoli\u00a0M, Garlan\u00a0D (2004) Synthesis of \u201ccorrect\u201d adaptors for protocol enhancement in component-based systems. In: SAVCBS 2004 specification and verification of component-based systems, p 79"},{"key":"233_CR11","first-page":"596","volume-title":"Proceedings of design automation conference\u201994","author":"D Beatty","year":"1994","unstructured":"Beatty\u00a0D, Bryant\u00a0R (1994) Formally verifying a microprocessor using a simulation methodology. In: Proceedings of design automation conference\u201994, pp 596\u2013602"},{"key":"233_CR12","first-page":"37","volume-title":"SIGSOFT FSE","author":"S Ben-David","year":"2011","unstructured":"Ben-David\u00a0S, Chechik\u00a0M, Gurfinkel\u00a0A, Uchitel\u00a0S (2011) CSSL: a logic for specifying conditional scenarios. In: Gyim\u00f3thy\u00a0T, Zeller\u00a0A (eds) SIGSOFT FSE. ACM, New York, pp 37\u201347. (Acceptance rate: 16\u00a0%. Scopus)"},{"key":"233_CR13","volume-title":"Proceedings of ICAPS","author":"P Bertoli","year":"2004","unstructured":"Bertoli\u00a0P, Pistore\u00a0M (2004) Planning with extended goals and partial observability. In: Proceedings of ICAPS, vol 4"},{"key":"233_CR14","volume-title":"Proceedings of the IJCAI\u201901 workshop on planning under uncertainty and incomplete information","author":"P Bertoli","year":"2001","unstructured":"Bertoli\u00a0P, Cimatti\u00a0A, Pistore\u00a0M, Roveri\u00a0M, Traverso\u00a0P (2001) MBP: a\u00a0model based planner. In: Proceedings of the IJCAI\u201901 workshop on planning under uncertainty and incomplete information"},{"key":"233_CR15","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1145\/1595696.1595719","volume-title":"Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering on European software engineering conference and foundations of software engineering symposium","author":"A Bertolino","year":"2009","unstructured":"Bertolino\u00a0A, Inverardi\u00a0P, Pelliccione\u00a0P, Tivoli\u00a0M (2009) Automatic synthesis of behavior protocols for composable web-services. In: Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering on European software engineering conference and foundations of software engineering symposium. ACM, New York, pp 141\u2013150"},{"key":"233_CR16","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-540-85361-9_14","volume-title":"Proceedings of the 19th international conference on concurrency theory, CONCUR \u201908","author":"K Chatterjee","year":"2008","unstructured":"Chatterjee\u00a0K, Henzinger TA, Jobstmann\u00a0B (2008) Environment assumptions for synthesis. In: Proceedings of the 19th international conference on concurrency theory, CONCUR \u201908. Springer, Berlin, pp 147\u2013161"},{"issue":"4","key":"233_CR17","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/990010.990011","volume":"12","author":"M Chechik","year":"2003","unstructured":"Chechik\u00a0M, Devereux\u00a0B, Easterbrook\u00a0S, Gurfinkel\u00a0A (2003) Multi-valued symbolic model-checking. ACM Trans Softw Eng Methodol 12(4):371\u2013408","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"233_CR18","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/978-3-540-71289-3_27","volume-title":"Proceedings of the 10th international conference on fundamental approaches to software engineering, FASE\u201907","author":"M Chechik","year":"2007","unstructured":"Chechik\u00a0M, Gheorghiu\u00a0M, Gurfinkel\u00a0A (2007) Finding environment guarantees. In: Proceedings of the 10th international conference on fundamental approaches to software engineering, FASE\u201907. Springer, Berlin, pp 352\u2013367"},{"key":"233_CR19","volume-title":"Model checking","author":"E Clarke","year":"1999","unstructured":"Clarke\u00a0E, Grumberg\u00a0O, Peled\u00a0D (1999) Model checking. MIT Press, Cambridge"},{"issue":"19","key":"233_CR20","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/244795.244800","volume":"2","author":"D Dams","year":"1997","unstructured":"Dams\u00a0D, Gerth\u00a0R, Grumberg\u00a0O (1997) Abstract interpretation of reactive systems. ACM Trans Program Lang Syst 2(19):253\u2013291","journal-title":"ACM Trans Program Lang Syst"},{"issue":"1","key":"233_CR21","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0167-6423(93)90021-G","volume":"20","author":"A Dardenne","year":"1993","unstructured":"Dardenne\u00a0A, van Lamsweerde\u00a0A, Fickas\u00a0S (1993) Goal-directed requirements acquisition. Sci Comput Program 20(1):3\u201350","journal-title":"Sci Comput Program"},{"key":"233_CR22","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1145\/239098.239131","volume-title":"Proc of 4th ACM SIGSOFT symposium on foundations of softw eng","author":"R Darimont","year":"1996","unstructured":"Darimont\u00a0R, van Lamsweerde\u00a0A (1996) Formal refinement patterns for goal-driven requirements elaboration. In: Proc of 4th ACM SIGSOFT symposium on foundations of softw eng, pp 179\u2013190"},{"issue":"5","key":"233_CR23","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1145\/503271.503226","volume":"26","author":"L Alfaro de","year":"2001","unstructured":"de Alfaro\u00a0L, Henzinger TA (2001) Interface automata. Softw Eng Notes 26(5):109\u2013120","journal-title":"Softw Eng Notes"},{"key":"233_CR24","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1145\/1985793.1985846","volume-title":"ICSE","author":"G Caso de","year":"2011","unstructured":"de Caso\u00a0G, Braberman VA, Garbervetsky\u00a0D, Uchitel\u00a0S (2011) Program abstractions for behaviour validation. In: Taylor RN, Gall\u00a0H, Medvidovic\u00a0N (eds) ICSE. ACM, New York, pp 381\u2013390"},{"issue":"1","key":"233_CR25","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1109\/TSE.2010.98","volume":"38","author":"G Caso de","year":"2012","unstructured":"de Caso\u00a0G, Braberman VA, Garbervetsky\u00a0D, Uchitel\u00a0S (2012) Automated abstractions for contract validation. IEEE Trans Softw Eng 38(1):141\u2013162","journal-title":"IEEE Trans Softw Eng"},{"key":"233_CR26","volume-title":"Ecoop 2004-object-oriented programming: 18th European conference: proceedings","author":"R DeLine","year":"2004","unstructured":"DeLine\u00a0R, Fahndrich\u00a0M (2004) Typestates for objects. In: Ecoop 2004-object-oriented programming: 18th European conference: proceedings, Oslo, Norway, June, 2004."},{"key":"233_CR27","first-page":"475","volume-title":"ASE","author":"N D\u2019Ippolito","year":"2008","unstructured":"D\u2019Ippolito\u00a0N, Fischbein\u00a0D, Chechik\u00a0M, Uchitel S (2008) Mtsa: the modal transition system analyser. In: ASE. IEEE Press, New York, pp 475\u2013476"},{"key":"233_CR28","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1145\/1985793.1985823","volume-title":"ICSE","author":"N D\u2019Ippolito","year":"2011","unstructured":"D\u2019Ippolito\u00a0N, Braberman VA, Piterman\u00a0N, Uchitel\u00a0S (2011) Synthesis of live behaviour models for fallible domains. In: Taylor RN, Gall\u00a0H, Medvidovic\u00a0N (eds) ICSE. ACM, New York, pp 211\u2013220"},{"key":"233_CR29","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito\u00a0N, Braberman\u00a0V, Piterman\u00a0N, Uchitel\u00a0S (2013) Synthesising non-anomalous event-based controllers for liveness goals. ACM Trans Softw Eng Methodol 22(1)","DOI":"10.1145\/2430536.2430543"},{"key":"233_CR30","author":"N D\u2019Ippolito","year":"2012","unstructured":"D\u2019Ippolito\u00a0N, Braberman\u00a0V, Piterman\u00a0N, Uchitel\u00a0S (2012) The modal transition system control problem. Lect Notes Comput Sci. doi: 10.1007\/978-3-642-32759-9_15","journal-title":"Lect Notes Comput Sci"},{"key":"233_CR31","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/s00766-002-0160-y","volume":"8","author":"MS Feather","year":"2003","unstructured":"Feather MS, Cornford SL (2003) Quantitative risk-based requirements reasoning. Requir Eng 8:248\u2013265","journal-title":"Requir Eng"},{"key":"233_CR32","first-page":"5","volume-title":"Proc of 8th intl work on software specification and design","author":"A Finkelstein","year":"1996","unstructured":"Finkelstein\u00a0A (1996) The London ambulance system case study. In: Proc of 8th intl work on software specification and design, pp\u00a05\u201319"},{"key":"233_CR33","unstructured":"Fischbein\u00a0D (2012) Foundations for behavioural model elaboration using modal transition systems. PhD thesis, Imperial College, London, UK"},{"key":"233_CR34","first-page":"297","volume-title":"SIGSOFT FSE","author":"D Fischbein","year":"2008","unstructured":"Fischbein\u00a0D, Uchitel\u00a0S (2008) On correct and complete strong merging of partial behaviour models. In: Harrold MJ, Murphy GC (eds) SIGSOFT FSE. ACM, New York, pp 297\u2013307"},{"key":"233_CR35","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/978-3-642-03466-4_14","volume-title":"ICTAC","author":"D Fischbein","year":"2009","unstructured":"Fischbein\u00a0D, Braberman VA, Uchitel\u00a0S (2009) A\u00a0sound observational semantics for modal transition systems. In: Leucker\u00a0M, Morgan\u00a0C (eds) ICTAC. Lecture notes in computer science, vol\u00a05684. Springer, Berlin, pp 215\u2013230"},{"issue":"2","key":"233_CR36","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/2089116.2089119","volume":"21","author":"D Fischbein","year":"2012","unstructured":"Fischbein\u00a0D, D\u2019Ippolito\u00a0N, Brunet\u00a0G, Chechik\u00a0M, Uchitel\u00a0S (2012) Weak alphabet merging of partial behavior models. ACM Trans Softw Eng Methodol 21(2):9","journal-title":"ACM Trans Softw Eng Methodol"},{"issue":"3\u20134","key":"233_CR37","first-page":"335","volume":"15","author":"M Fitting","year":"1991","unstructured":"Fitting\u00a0M (1991) Many-valued modal logics. Fundam Inform 15(3\u20134):335\u2013350","journal-title":"Fundam Inform"},{"key":"233_CR38","first-page":"1070","volume-title":"Proc of 5th int conference on logic programming","author":"M Gelfond","year":"1988","unstructured":"Gelfond\u00a0M, Lifschitz\u00a0V (1988) The stable model semantics for logic programming. In: Kowalski RA, Bowen\u00a0K (eds) Proc of 5th int conference on logic programming, pp 1070\u20131080"},{"key":"233_CR39","first-page":"257","volume-title":"Proceedings of the 9th joint meeting of the European software engineering conference and ACM SIGSOFT symposium on the foundations of software engineering (ESEC\/FSE\u201903)","author":"D Giannakopoulou","year":"2003","unstructured":"Giannakopoulou\u00a0D, Magee\u00a0J (2003) Fluent model checking for event-based systems. In: Proceedings of the 9th joint meeting of the European software engineering conference and ACM SIGSOFT symposium on the foundations of software engineering (ESEC\/FSE\u201903). ACM, New York, pp 257\u2013266"},{"key":"233_CR40","author":"W Grieskamp","year":"2011","unstructured":"Grieskamp\u00a0W, Kicillof\u00a0N, Stobie\u00a0K, Braberman\u00a0V (2011) Model-based quality assurance of protocol documentation: tools and methodology. Soft Test Verif Reliab. doi: 10.1002\/stvr.427","journal-title":"Soft Test Verif Reliab"},{"key":"233_CR41","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/978-3-540-24730-2_34","volume-title":"Proceedings of 10th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201904)","author":"A Gurfinkel","year":"2004","unstructured":"Gurfinkel\u00a0A, Chechik\u00a0M (2004) How vacuous is vacuous? In: Proceedings of 10th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201904), Barcelona, Spain. LNCS, vol 2988. Springer, Berlin, pp 451\u2013466"},{"key":"233_CR42","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19029-2","volume-title":"Come, let\u2019s play\u2014scenario-based programming using LSCs and the play-engine","author":"D Harel","year":"2003","unstructured":"Harel\u00a0D (2003) Come, let\u2019s play\u2014scenario-based programming using LSCs and the play-engine. Springer, Berlin"},{"key":"233_CR43","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/978-3-642-02161-9_6","volume-title":"Software engineering for self-adaptive systems","author":"W Heaven","year":"2009","unstructured":"Heaven\u00a0W, Sykes\u00a0D, Magee\u00a0J, Kramer\u00a0J (2009) A\u00a0case study in goal-driven architectural adaptation. In: Software engineering for self-adaptive systems. Springer, Berlin, pp 109\u2013127"},{"key":"233_CR44","volume-title":"Communicating sequential processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice Hall, New York"},{"key":"233_CR45","volume-title":"IEEE standard glossary of software engineering terminology","author":"IEEE","year":"1990","unstructured":"IEEE (1990) IEEE standard glossary of software engineering terminology"},{"key":"233_CR46","unstructured":"ITU (2000) Message sequence charts. Technical report recommendation Z.120, International Telecommunications Union, Telecommunication Standardisation Sector"},{"key":"233_CR47","volume-title":"Software requirements & specifications\u2014a\u00a0lexicon of practice, principles and prejudices","author":"M Jackson","year":"1995","unstructured":"Jackson\u00a0M (1995) Software requirements & specifications\u2014a\u00a0lexicon of practice, principles and prejudices. Addison-Wesley, Reading"},{"key":"233_CR48","first-page":"283","volume-title":"Proceedings of the 17th international conference on software engineering, ICSE\u201995","author":"M Jackson","year":"1995","unstructured":"Jackson\u00a0M (1995) The world and the machine. In: Proceedings of the 17th international conference on software engineering, ICSE\u201995. ACM, New York, pp 283\u2013292"},{"issue":"7","key":"233_CR49","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"R Keller","year":"1976","unstructured":"Keller\u00a0R (1976) Formal verification of parallel programs. Commun ACM 19(7):371\u2013384","journal-title":"Commun ACM"},{"issue":"1","key":"233_CR50","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/BF03037383","volume":"4","author":"RA Kowalski","year":"1986","unstructured":"Kowalski RA, Sergot\u00a0M (1986) A\u00a0logic-based calculus of events. New Gener Comput 4(1):67\u201395","journal-title":"New Gener Comput"},{"key":"233_CR51","volume-title":"IEE proc, part\u00a0E","author":"J Kramer","year":"1983","unstructured":"Kramer\u00a0J, Magee\u00a0J, Sloman\u00a0M (1983) Conic: an integrated approach to distributed computer control systems. In: IEE proc, part\u00a0E, vol 130"},{"key":"233_CR52","first-page":"83","volume":"16","author":"SA Kripke","year":"1963","unstructured":"Kripke SA (1963) Semantical considerations on modal logic. Acta Philos Fenn 16:83\u201394","journal-title":"Acta Philos Fenn"},{"key":"233_CR53","first-page":"203","volume-title":"Proceedings of 3rd annual symposium on logic in computer science (LICS\u201988)","author":"KG Larsen","year":"1988","unstructured":"Larsen KG, Thomsen\u00a0B (1988) A\u00a0modal process logic. In: Proceedings of 3rd annual symposium on logic in computer science (LICS\u201988). IEEE Comput Soc, Los Alamitos, pp 203\u2013210"},{"key":"233_CR54","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1109\/LICS.1990.113738","volume-title":"Proceedings of the 5th annual IEEE symposium on logic in computer science (LICS\u201990)","author":"K Larsen","year":"1990","unstructured":"Larsen\u00a0K, Xinxin\u00a0L (1990) Equation solving using modal transition systems. In: Proceedings of the 5th annual IEEE symposium on logic in computer science (LICS\u201990). IEEE Comput Soc, Los Alamitos, pp 108\u2013117"},{"key":"233_CR55","series-title":"LNCS","first-page":"13","volume-title":"Tools and algorithms for construction and analysis of systems (TACAS\u201995)","author":"KG Larsen","year":"1995","unstructured":"Larsen KG, Steffen\u00a0B, Weise\u00a0C (1995) A\u00a0constraint oriented proof methodology based on modal transition systems. In: Tools and algorithms for construction and analysis of systems (TACAS\u201995). LNCS. Springer, Berlin, pp 13\u201328"},{"key":"233_CR56","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1145\/587051.587070","volume-title":"Proc of 10th ACM SIGSOFT symposium on foundations of software engineering","author":"E Letier","year":"2002","unstructured":"Letier\u00a0E, Van Lamsweerde\u00a0A (2002) Deriving operational software specifications from system goals. In: Proc of 10th ACM SIGSOFT symposium on foundations of software engineering, pp 119\u2013128"},{"issue":"2","key":"233_CR57","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10515-008-0027-7","volume":"15","author":"E Letier","year":"2008","unstructured":"Letier\u00a0E, Kramer\u00a0J, Magee\u00a0J, Uchitel\u00a0S (2008) Deriving event-based transition systems from goal-oriented requirements models. Autom Softw Eng 15(2):175\u2013206","journal-title":"Autom Softw Eng"},{"key":"233_CR58","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/0167-6423(95)96871-J","volume":"25","author":"DL Parnas","year":"1995","unstructured":"Parnas DL, Madey\u00a0J (1995) Functional documents for computer systems. Sci Comput Program 25:41\u201361","journal-title":"Sci Comput Program"},{"key":"233_CR59","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer\u00a0B (1992) Applying \u2018design by contract\u2019. Computer 25:40\u201351","journal-title":"Computer"},{"key":"233_CR60","volume-title":"Communication and concurrency","author":"R Milner","year":"1989","unstructured":"Milner\u00a0R (1989) Communication and concurrency. Prentice-Hall, New York"},{"key":"233_CR61","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/11609773_24","volume":"3855","author":"N Piterman","year":"2006","unstructured":"Piterman\u00a0N, Pnueli\u00a0A, Sa\u2019ar\u00a0Y (2006) Synthesis of reactive (1) designs. Lect Notes Comput Sci 3855:364\u2013380","journal-title":"Lect Notes Comput Sci"},{"key":"233_CR62","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1145\/75277.75293","volume-title":"Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on principles of programming languages","author":"A Pnueli","year":"1989","unstructured":"Pnueli\u00a0A, Rosner\u00a0R (1989) On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp 179\u2013190"},{"key":"233_CR63","volume-title":"Software engineering: a\u00a0practitioner\u2019s approach","author":"RS Pressman","year":"2010","unstructured":"Pressman RS (2010) Software engineering: a\u00a0practitioner\u2019s approach, 7th edn. McGraw-Hill, New York","edition":"7"},{"issue":"1","key":"233_CR64","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"PJG Ramadge","year":"1989","unstructured":"Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81\u201398","journal-title":"Proc IEEE"},{"issue":"1","key":"233_CR65","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1109\/32.341844","volume":"21","author":"DS Rosenblum","year":"1995","unstructured":"Rosenblum DS (1995) A\u00a0practical approach to programming with assertions. IEEE Trans Softw Eng 21(1):19\u201331","journal-title":"IEEE Trans Softw Eng"},{"issue":"1","key":"233_CR66","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/s10270-010-0148-x","volume":"10","author":"M Sassolas","year":"2011","unstructured":"Sassolas\u00a0M, Chechik\u00a0M, Uchitel\u00a0S (2011) Exploring inconsistencies between modal transition systems. Softw Syst Model 10(1):117\u2013142","journal-title":"Softw Syst Model"},{"key":"233_CR67","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1145\/1368088.1368095","volume-title":"ICSE","author":"G Sibay","year":"2008","unstructured":"Sibay\u00a0G, Uchitel\u00a0S, Braberman VA (2008) Existential live sequence charts revisited. In: Sch\u00e4fer\u00a0W, Dwyer MB, Gruhn\u00a0V (eds) ICSE. ACM, New York, pp 41\u201350"},{"key":"233_CR68","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/1292316.1292318","volume-title":"SAVCBS","author":"D Sykes","year":"2007","unstructured":"Sykes\u00a0D, Heaven\u00a0W, Magee\u00a0J, Kramer\u00a0J (2007) Plan-directed architectural change for autonomous systems. In: Poetzsch-Heffter\u00a0A (ed) SAVCBS. ACM, New York, pp 15\u201321"},{"key":"233_CR69","first-page":"43","volume-title":"Proceedings of 12th ACM SIGSOFT international symposium on foundations of software engineering","author":"S Uchitel","year":"2004","unstructured":"Uchitel\u00a0S, Chechik\u00a0M (2004) Merging partial behavioural models. In: Proceedings of 12th ACM SIGSOFT international symposium on foundations of software engineering, pp 43\u201352"},{"key":"233_CR70","first-page":"19","volume-title":"ESEC\/SIGSOFT FSE","author":"S Uchitel","year":"2003","unstructured":"Uchitel\u00a0S, Kramer\u00a0J, Magee\u00a0J (2003) Behaviour model elaboration using partial labelled transition systems. In: ESEC\/SIGSOFT FSE. ACM, New York, pp 19\u201327"},{"key":"233_CR71","first-page":"34","volume-title":"ICSE","author":"S Uchitel","year":"2007","unstructured":"Uchitel\u00a0S, Brunet\u00a0G, Chechik\u00a0M (2007) Behaviour model synthesis from properties and scenarios. In: ICSE. IEEE Comput Soc, Los Alamitos, pp 34\u201343"},{"issue":"3","key":"233_CR72","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1109\/TSE.2008.107","volume":"35","author":"S Uchitel","year":"2009","unstructured":"Uchitel\u00a0S, Brunet\u00a0G, Chechik\u00a0M (2009) Synthesis of partial behavior models from properties and scenarios. IEEE Trans Softw Eng 35(3):384\u2013406","journal-title":"IEEE Trans Softw Eng"},{"issue":"3","key":"233_CR73","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"RJ Gabbeek van","year":"1996","unstructured":"van Gabbeek RJ, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3):555\u2013600","journal-title":"J ACM"},{"key":"233_CR74","volume-title":"Proceedings of the fifth IEEE international symposium on requirements engineering","author":"A Lamsweerde van","year":"2001","unstructured":"van Lamsweerde\u00a0A (2001) Goal-oriented requirements engineering: a\u00a0guided tour. In: Proceedings of the fifth IEEE international symposium on requirements engineering. IEEE Comput Soc, Washington"},{"key":"233_CR75","volume-title":"Requirements engineering: from system goals to UML models to software specifications","author":"A Lamsweerde van","year":"2009","unstructured":"van Lamsweerde\u00a0A (2009) Requirements engineering: from system goals to UML models to software specifications. Wiley, New York"},{"key":"233_CR76","doi-asserted-by":"crossref","first-page":"978","DOI":"10.1109\/32.879820","volume":"26","author":"A Lamsweerde van","year":"2000","unstructured":"van Lamsweerde\u00a0A, Letier\u00a0E (2000) Handling obstacles in goal-oriented requirements engineering. IEEE Trans Softw Eng 26:978\u20131005","journal-title":"IEEE Trans Softw Eng"},{"key":"233_CR77","first-page":"218","volume-title":"Requirements engineering conference, 2004","author":"HT Van","year":"2004","unstructured":"Van HT, van Lamsweerde\u00a0A, Massonet\u00a0P, Ponsard\u00a0C (2004) Goal-oriented requirements animation. In: Requirements engineering conference, 2004, pp 218\u2013228"},{"key":"233_CR78","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/1984708.1984721","volume-title":"Proceedings of the 1st workshop on developing tools as Plug-ins, TOPI \u201911","author":"E Zoppi","year":"2011","unstructured":"Zoppi\u00a0E, Braberman\u00a0V, de Caso\u00a0G, Garbervetsky\u00a0D, Uchitel\u00a0S (2011) Contractor.net: inferring typestate properties to enrich code contracts. In: Proceedings of the 1st workshop on developing tools as Plug-ins, TOPI \u201911. ACM, New York, pp 44\u201347"}],"container-title":["Computer Science - Research and Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00450-012-0233-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00450-012-0233-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00450-012-0233-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,30]],"date-time":"2022-01-30T13:51:06Z","timestamp":1643550666000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00450-012-0233-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,25]]},"references-count":78,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["233"],"URL":"https:\/\/doi.org\/10.1007\/s00450-012-0233-1","relation":{},"ISSN":["1865-2034","1865-2042"],"issn-type":[{"value":"1865-2034","type":"print"},{"value":"1865-2042","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,25]]}}}