{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:21:19Z","timestamp":1759033279444},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,2,12]],"date-time":"2009-02-12T00:00:00Z","timestamp":1234396800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Requirements Eng"],"published-print":{"date-parts":[[2009,7]]},"DOI":"10.1007\/s00766-009-0074-z","type":"journal-article","created":{"date-parts":[[2009,2,11]],"date-time":"2009-02-11T06:08:50Z","timestamp":1234332530000},"page":"129-153","source":"Crossref","is-referenced-by-count":6,"title":["Methodologies to evolve formal specifications through refinement and retrenchment in an analysis\u2013revision cycle"],"prefix":"10.1007","volume":"14","author":[{"given":"Jorge","family":"Garc\u00eda-Duque","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9 J.","family":"Pazos-Arias","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mart\u00edn","family":"L\u00f3pez-Nores","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yolanda","family":"Blanco-Fern\u00e1ndez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"Fern\u00e1ndez-Vilas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rebeca P.","family":"D\u00edaz-Redondo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Ramos-Cabrer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Gil-Solla","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,2,12]]},"reference":[{"key":"74_CR1","doi-asserted-by":"crossref","unstructured":"Letier E, van Lamsweerde A (2002) Deriving operational software specifications from system goals. In: Proceedings of 10th ACM SIGSOFT symposium on the foundations of software engineering, Charleston, USA, pp 119\u2013128","DOI":"10.1145\/587051.587070"},{"key":"74_CR2","unstructured":"Liu S (2002) Capturing complete and accurate requirements by refinement. In: Proceedings of 8th IEEE international conference on engineering of complex computer systems. Greenbelt, USA, pp 57\u201367"},{"key":"74_CR3","doi-asserted-by":"crossref","unstructured":"d\u2019Avila Garcez A, Russo A, Nuseibeh B, Kramer J (2001) An analysis\u2013revision cycle to evolve requirements specifications. In: Proceedings of 16th IEEE international conference on automated software engineering. San Diego, USA, pp 354\u2013358","DOI":"10.1109\/ASE.2001.989828"},{"issue":"1","key":"74_CR4","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1049\/ip-sen:20030207","volume":"150","author":"A d\u2019Avila Garcez","year":"2003","unstructured":"d\u2019Avila Garcez A, Russo A, Nuseibeh B, Kramer J (2003) Combining abductive reasoning and inductive learning to evolve requirements specifications. IEE Proc Softw 150(1):25\u201338","journal-title":"IEE Proc Softw"},{"key":"74_CR5","unstructured":"Kakas A, Kowalski R, Toni F (1998) Handbook of logic in artificial intelligence and logic programming, vol 5. The role of abduction in logic programming. Oxford University Press, New York, pp 235\u2013324"},{"key":"74_CR6","unstructured":"Mitchell T (1997) Machine learning. McGraw Hill, NY"},{"key":"74_CR7","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/PL00003939","volume":"13","author":"JJ Pazos-Arias","year":"2001","unstructured":"Pazos-Arias JJ, Garc\u00eda-Duque J (2001) SCTL-MUS: a formal methodology for software development of distributed systems: a case study. Formal Aspects Comput 13:50\u201391","journal-title":"Formal Aspects Comput"},{"key":"74_CR8","unstructured":"Kleene S (1952) Introduction to metamathematics, vol 1 of Bibliotheca mathematica. North-Holland"},{"key":"74_CR9","doi-asserted-by":"crossref","unstructured":"Huth MRA, Jagadeesan R, Schmidt DA (2001) Modal transition systems: a foundation for three-valued program analysis. In: Proceedings of European Symposium on programming, in conjunction with ETAPS. Genoa, Italy, pp 155\u2013169","DOI":"10.1007\/3-540-45309-1_11"},{"issue":"6","key":"74_CR10","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1093\/logcom\/1.6.797","volume":"1","author":"M Fitting","year":"1991","unstructured":"Fitting M (1991) Kleene\u2019s logic, generalized. J Logic Comput 1(6):797\u2013810","journal-title":"J Logic Comput"},{"key":"74_CR11","doi-asserted-by":"crossref","unstructured":"Uchitel S, Kramer J (2001) A workbench for synthesising behaviour models from scenarios. In: Proceedings of 23rd international conference on software engineering. Toronto, Canada, pp 188\u2013197","DOI":"10.1109\/ICSE.2001.919093"},{"key":"74_CR12","doi-asserted-by":"crossref","unstructured":"Whittle J, Schumann J (2000) Generating statechart designs from scenarios. In: Proceedings of 22nd international conference on software engineering. Limerick, Ireland, pp 314\u2013323","DOI":"10.1145\/337180.337217"},{"issue":"2","key":"74_CR13","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1093\/logcom\/exi076","volume":"16","author":"J Garc\u00eda-Duque","year":"2006","unstructured":"Garc\u00eda-Duque J, L\u00f3pez-Nores M, Pazos-Arias JJ, Fern\u00e1ndez-Vilas A, D\u00edaz-Redondo RP, Gil-Solla A, Blanco-Fern\u00e1ndez Y, Ramos-Cabrer M (2006) A six-valued logic to reason about uncertainty and inconsistency in requirements specifications. J Logic Comput 16(2):227\u2013255","journal-title":"J Logic Comput"},{"issue":"2","key":"74_CR14","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/S0164-1212(03)00067-0","volume":"70","author":"A Fern\u00e1ndez-Vilas","year":"2004","unstructured":"Fern\u00e1ndez-Vilas A, Pazos-Arias JJ, Gil-Solla A, D\u00edaz-Redondo RP, Garc\u00eda-Duque J, Barrag\u00e1ns-Mart\u00ednez AB (2004) Incremental specification with SCTL\/MUS-T: a case study. J Syst Softw 70(2):189\u2013208","journal-title":"J Syst Softw"},{"key":"74_CR15","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1017\/S0960129504004268","volume":"14","author":"MRA Huth","year":"2004","unstructured":"Huth MRA, Jagadeesan R, Schmidt DA (2004) A domain equation for refinement of partial systems. Math Struct Comput Sci 14:469\u2013505","journal-title":"Math Struct Comput Sci"},{"key":"74_CR16","unstructured":"Belnap ND (1977) Modern uses of multiple-valued logic, chapter a useful four-valued logic. Reidel, pp 7\u201337"},{"key":"74_CR17","unstructured":"Morgan C (1990) Programing from specifications. Prentice Hall, Englewood cliffs"},{"key":"74_CR18","doi-asserted-by":"crossref","unstructured":"Garc\u00eda-Duque J, Pazos-Arias JJ, Barrag\u00e1ns-Mart\u00ednez AB (2002) An analysis\u2013revision cycle to evolve requirements specifications by using the SCTL-MUS methodology. In: Proceedings of 10th IEEE international conference on requirements engineering. Essen, Germany, pp 282\u2013288","DOI":"10.1109\/ICRE.2002.1048539"},{"issue":"6","key":"74_CR19","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1109\/52.469758","volume":"12","author":"M Shaw","year":"1995","unstructured":"Shaw M (1995) Comparing architectural design styles. IEEE Softw 12(6):27\u201341","journal-title":"IEEE Softw"},{"issue":"8","key":"74_CR20","doi-asserted-by":"crossref","first-page":"1141","DOI":"10.1016\/j.jss.2005.12.019","volume":"79","author":"M L\u00f3pez-Nores","year":"2006","unstructured":"L\u00f3pez-Nores M, Pazos-Arias JJ, Garc\u00eda-Duque J, Blanco-Fern\u00e1ndez Y, Ramos-Cabrer M, Gil-Solla A, Fern\u00e1ndez-Vilas A, D\u00edaz-Redondo RP (2006) Formal specification applied to distributed multiuser services: experiences in collaborative t-learning. J Syst Softw 79(8):1141\u20131155","journal-title":"J Syst Softw"},{"issue":"8","key":"74_CR21","doi-asserted-by":"crossref","first-page":"845","DOI":"10.1002\/spe.719","volume":"36","author":"JJ Pazos-Arias","year":"2006","unstructured":"Pazos-Arias JJ, L\u00f3pez-Nores M, Garc\u00eda-Duque J, Gil-Solla A, Ramos-Cabrer M, Blanco-Fern\u00e1ndez Y, D\u00edaz-Redondo RP, Fern\u00e1ndez-Vilas A (2006) ATLAS: a framework to provide multiuser and distributed t-learning services over MHP. Softw Prac Exp 36(8):845\u2013869","journal-title":"Softw Prac Exp"},{"key":"74_CR22","doi-asserted-by":"crossref","unstructured":"Swamy G (1996) Incremental methods for formal verification and logic synthesis. PhD thesis, University of California at Berkeley","DOI":"10.2139\/ssrn.3702088"},{"issue":"4","key":"74_CR23","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1142\/S021819400500249X","volume":"15","author":"RP D\u00edaz-Redondo","year":"2005","unstructured":"D\u00edaz-Redondo RP, Pazos-Arias JJ, Fern\u00e1ndez-Vilas A, Garc\u00eda-Duque J, Gil-Solla A (2005) ARIFS methodology: reusing incomplete models at the requirements specification stage. Int J Softw Eng Knowl Eng 15(4):607\u2013645","journal-title":"Int J Softw Eng Knowl Eng"},{"key":"74_CR24","doi-asserted-by":"crossref","unstructured":"L\u00f3pez-Nores M, D\u00edaz-Redondo RP, Pazos-Arias JJ, Garc\u00eda-Duque J (2004) An improved repository system for effective and efficient reuse of formal verification efforts. In: Proceedings of 11th Asia-Pacific software engineering conference Busan, South Korea, pp 38\u201345","DOI":"10.1109\/APSEC.2004.28"},{"issue":"6","key":"74_CR25","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1109\/32.142870","volume":"18","author":"S Fickas","year":"1992","unstructured":"Fickas S, Helm BR (1992) Knowledge representation and reasoning in the design of composite systems. IEEE Trans Softw Eng 18(6):470\u2013482","journal-title":"IEEE Trans Softw Eng"},{"key":"74_CR26","unstructured":"Easterbrook S (1993) Social and technological issues in requirements engineering, chapter Resolving requirements conflicts with computer-supported negotiation. Academic Press, Dublin, pp 41\u201365"},{"issue":"2","key":"74_CR27","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S Owre","year":"1995","unstructured":"Owre S, Rushby J, Shankar N, von Henke F (1995) Formal verification for fault-tolerant architecture: prolegomena to the design of PVS. IEEE Trans Softw Eng 21(2):107\u2013125","journal-title":"IEEE Trans Softw Eng"},{"key":"74_CR28","unstructured":"Clarke E, Grumberg O, Peled D (2000) Model checking. The MIT Press, Cambridge"},{"key":"74_CR29","unstructured":"Tran Van H, van Lamsweerde A, Massonet P, Ponsard C (2004) Goal-oriented requirements animation. In: 12th IEEE Intl. Conf. on Requirements Engineering. Kyoto, Japan, pp 218\u2013228"},{"key":"74_CR30","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1016\/S0950-5849(03)00100-9","volume":"45","author":"D Zowghi","year":"2003","unstructured":"Zowghi D, Gervasi V (2003) On the interplay between consistency, completeness and correctness in requirements evolution. Inf Softw Technol 45:993\u20131009","journal-title":"Inf Softw Technol"},{"key":"74_CR31","unstructured":"Satoh K (2003) Computing minimal revised specifications by default logic. In: Proceedings of workshop on intelligent technologies in software engineering, in conjunction with ESEC\/FSE. Helsinki, Finland, pp 7\u201312"},{"issue":"10","key":"74_CR32","doi-asserted-by":"crossref","first-page":"978","DOI":"10.1109\/32.879820","volume":"26","author":"A Lamsweerde van","year":"2000","unstructured":"van Lamsweerde A, Letier E (2000) Handling obstacles in goal-oriented requirements engineering. IEEE Trans Softw Eng 26(10):978\u20131005","journal-title":"IEEE Trans Softw Eng"},{"key":"74_CR33","unstructured":"M\u00e4kinen E, Syst\u00e4 T (2001) MAS\u2014an interactive synthesizer to support behavioral modelling in UML. In: Proceedings of 23rd international conference on software engineering. Toronto, Canada, pp 15\u201324"},{"key":"74_CR34","doi-asserted-by":"crossref","unstructured":"Uchitel S, Kramer J, Magee J (2003) Behaviour model elaboration using partial labelled transition systems. In: Proceedngs of 4th joint ESEC\/FSE meeting. Helsinki, Finland, pp 19\u201327","DOI":"10.1145\/940071.940076"},{"key":"74_CR35","doi-asserted-by":"crossref","unstructured":"van Lamsweerde A (2004) Goal-oriented requirements engineering: a roundtrip from research to practice. In: Proceedings of 12th IEEE international conference on requirements engineering. Kyoto, Japan, pp 4\u20138","DOI":"10.1109\/ICRE.2004.1335648"},{"key":"74_CR36","doi-asserted-by":"crossref","unstructured":"Back R, Akademi A, von Wright J, Schneider F, Gries D (1998) Refinement calculus: a systematic introduction. Springer, Berlin","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"74_CR37","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1016\/j.scico.2007.04.002","volume":"67","author":"R Banach","year":"2007","unstructured":"Banach R, Poppleton M, Jeske C, Stepney S (2007) Engineering and theoretical underpinnings of retrenchment. Sci Comput Program 67:301\u2013329","journal-title":"Sci Comput Program"},{"key":"74_CR38","unstructured":"Sannella D (1999) Algebraic specification and program development by stepwise refinement. In: Proceedings of 9th international workshop on logic programming synthesis and transformation. Venice, Italy, pp 1\u20139"},{"key":"74_CR39","doi-asserted-by":"crossref","unstructured":"Pons C (2006) Heuristics on the definition of UML refinement patterns. In: Proceedings of 32nd International conference on current trends in theory and practice of computer science, Merin, Czech Republic, pp 461\u2013470","DOI":"10.1007\/11611257_44"},{"key":"74_CR40","doi-asserted-by":"crossref","unstructured":"Letier E, van Lamsweerde A (2002) Agent-based tactics for goal-oriented requirements elaboration. In: Proceedings of 24th international conference on software engineering. Orlando, USA, pp 83\u201393","DOI":"10.1145\/581352.581353"},{"issue":"2","key":"74_CR41","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/s00766-007-0056-y","volume":"13","author":"IJ Jureta","year":"2008","unstructured":"Jureta IJ, Faulkner S, Schobbens P-Y (2008) Clear justification of modeling decisions for goal-oriented requirements engineering. Requir Eng 13(2):87\u2013115","journal-title":"Requir Eng"},{"key":"74_CR42","doi-asserted-by":"crossref","unstructured":"Balzer R (1991) Tolerating inconsistency. In: Proceedings of 13th international conference on software engineering. Austin, USA, pp 158\u2013165","DOI":"10.1109\/ICSE.1991.130638"},{"issue":"2","key":"74_CR43","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/S0164-1212(01)00036-X","volume":"58","author":"B Nuseibeh","year":"2001","unstructured":"Nuseibeh B, Easterbrook S, Russo A (2001) Making inconsistency respectable in software development. J Syst Softw 58(2):171\u2013180","journal-title":"J Syst Softw"},{"key":"74_CR44","doi-asserted-by":"crossref","unstructured":"Arieli O, Avron A (1994) Logical bilattices and inconsistent data. In: Proceedings of 9th IEEE annual symposium on logic in computer science. Paris, France, pp 468\u2013476","DOI":"10.1109\/LICS.1994.316044"},{"key":"74_CR45","doi-asserted-by":"crossref","unstructured":"Easterbrook S, Chechik M (2001) A framework for multi-valued reasoning over inconsistent viewpoints. In: Proceedings of 23rd international conference on software engineering. Toronto, Canada, pp 411\u2013420","DOI":"10.1109\/ICSE.2001.919114"},{"key":"74_CR46","doi-asserted-by":"crossref","unstructured":"Konieczny S, Marquis P (2002) Three-valued logics for inconsistency handling. In: Proceedings of European Conference on logics in artificial intelligence. Cosenza, Italy, pp 322\u2013344","DOI":"10.1007\/3-540-45757-7_28"},{"issue":"4","key":"74_CR47","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1016\/j.infsof.2007.02.001","volume":"50","author":"AB Barrag\u00e1ns-Mart\u00ednez","year":"2008","unstructured":"Barrag\u00e1ns-Mart\u00ednez AB, Pazos-Arias JJ, Fern\u00e1ndez-Vilas A, Garc\u00eda-Duque J, L\u00f3pez-Nores M, D\u00edaz-Redondo RP, Blanco-Fern\u00e1ndez Y (2008) On the interplay between inconsistency and incompleteness in multi-perspective requirements specifications. Inf Softw Technol 50(4):296\u2013321","journal-title":"Inf Softw Technol"},{"issue":"3","key":"74_CR48","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/s00766-008-0064-6","volume":"13","author":"AB Barrag\u00e1ns-Mart\u00ednez","year":"2008","unstructured":"Barrag\u00e1ns-Mart\u00ednez AB, Pazos-Arias JJ, Fern\u00e1ndez-Vilas A, Garc\u00eda-Duque J, L\u00f3pez-Nores M, D\u00edaz-Redondo RP, Blanco-Fern\u00e1ndez Y (2008) Composing requirements specifications from multiple prioritized sources. Requir Eng 13(3):187\u2013206","journal-title":"Requir Eng"}],"container-title":["Requirements Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00766-009-0074-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00766-009-0074-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00766-009-0074-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,1]],"date-time":"2021-10-01T13:31:23Z","timestamp":1633095083000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00766-009-0074-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2,12]]},"references-count":48,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,7]]}},"alternative-id":["74"],"URL":"https:\/\/doi.org\/10.1007\/s00766-009-0074-z","relation":{},"ISSN":["0947-3602","1432-010X"],"issn-type":[{"value":"0947-3602","type":"print"},{"value":"1432-010X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,2,12]]}}}