{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T14:15:22Z","timestamp":1740147322460,"version":"3.37.3"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T00:00:00Z","timestamp":1620086400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T00:00:00Z","timestamp":1620086400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["SOCA"],"published-print":{"date-parts":[[2021,9]]},"DOI":"10.1007\/s11761-021-00314-4","type":"journal-article","created":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T04:09:00Z","timestamp":1620101340000},"page":"205-230","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Event-B formal model for a system reconfiguration pattern and its instantiation: application to Web services compensation"],"prefix":"10.1007","volume":"15","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4582-9712","authenticated-orcid":false,"given":"Yamine","family":"Ait-Ameur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillaume","family":"Babin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Pantel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,5,4]]},"reference":[{"key":"314_CR1","first-page":"1","volume-title":"Correct software in web applications and web services","author":"I A\u00eft-Sadoune","year":"2015","unstructured":"A\u00eft-Sadoune I, Ait-Ameur Y (2015) Formal modelling and verification of transactional web service composition: a refinement and proof approach with event-b. In: Thalheim B, Schewe K-D, Prinz A, Buchberger B (eds) Correct software in web applications and web services. Springer, Berlin, pp 1\u201327"},{"issue":"6","key":"314_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial J-R, Butler M, Hallerstede S, Ho\u00e0ng TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. Int J Softw Tools Technol Transf 12(6):447\u2013466","journal-title":"Int J Softw Tools Technol Transf"},{"key":"314_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial J-R (1996) The B-book: assigning programs to meanings. Cambridge University Press, Cambridge"},{"key":"314_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: system and software engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial J-R (2010) Modeling in Event-B: system and software engineering, 1st edn. Cambridge University Press, New York","edition":"1"},{"key":"314_CR5","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-14977-6_6","volume-title":"Distributed computing and internet technology","author":"X An","year":"2015","unstructured":"An X, Delaval G, Diguet J-P, Gamati\u00e9 A, Gueye S, Marchand H, de Palma N, Rutten E (2015) Discrete control-based design of adaptive and autonomic computing systems. In: Raja N, Gautam B, Ranjan PM (eds) Distributed computing and internet technology, vol 8956. Lecture notes in computer science. Springer, Berlin, pp 93\u2013113"},{"issue":"1","key":"314_CR6","first-page":"1","volume":"77","author":"J-R Abrial","year":"2007","unstructured":"Abrial J-R, Hallerstede S (2007) Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundam Inform 77(1):1\u201328","journal-title":"Fundam Inform"},{"key":"314_CR7","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1016\/j.scico.2015.12.004","volume":"121","author":"Y Ait-Ameur","year":"2016","unstructured":"Ait-Ameur Y, M\u00e9ry D (2016) Making explicit domain knowledge in formal system development. Sci Comput Program 121:100\u2013127","journal-title":"Sci Comput Program"},{"key":"314_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-25942-0_4","volume-title":"Dependable software engineering: theories, tools, and applications","author":"G Babin","year":"2015","unstructured":"Babin G, A\u00eft-Ameur Y, Nakajima S, Pantel M (2015) Refinement and proof based development of systems characterized by continuous functions. In: Li X, Liu Z, Yi W (eds) Dependable software engineering: theories, tools, and applications, vol 9409. Lecture notes in computer science. Springer, Berlin, pp 55\u201370"},{"key":"314_CR9","doi-asserted-by":"crossref","unstructured":"Babin G, A\u00eft-Ameur Y, Marc P (2015) Formal verification of runtime compensation of web service compositions: a refinement and proof based proposal with Event-B. In: IEEE international conference on services computing (SCC), pp 98\u2013105","DOI":"10.1109\/SCC.2015.23"},{"key":"314_CR10","doi-asserted-by":"crossref","unstructured":"Babin G, A\u00eft-Ameur Y, Pantel M (2016) Correct instantiation of a system reconfiguration pattern: a proof and refinement-based approach. In: 2016 IEEE 17th international symposium on high assurance systems engineering (HASE), pp 31\u201338","DOI":"10.1109\/HASE.2016.47"},{"key":"314_CR11","volume-title":"Trustworthy cyber-physical systems engineering, computer and information science series, chapter 4","author":"G Babin","year":"2016","unstructured":"Babin G, Yamine A-A, Marc P (2016) A generic model for system substitution. In: Alexander R, Fuyuki I (eds) Trustworthy cyber-physical systems engineering, computer and information science series, chapter 4. Chapman and Hall\/CRC, London"},{"key":"314_CR12","doi-asserted-by":"crossref","unstructured":"Babin G, A\u00eft-Ameur Y, Pantel M (2017) Web service compensation at runtime: formal modeling and verification using the event-b refinement and proof based formal method. In: IEEE transactions on services computing\u2014special issue on advances in web services research","DOI":"10.1109\/TSC.2016.2594782"},{"key":"314_CR13","doi-asserted-by":"crossref","unstructured":"Babin G, A\u00eft-Ameur Y, Singh NK, Pantel M(2016) Abstract state machines, Alloy, B, TLA, VDM, and Z: 5th international conference, ABZ 2016, Linz, Austria, May 23\u201327, 2016, proceedings, chapter handling continuous functions in hybrid systems reconfigurations: a formal Event-B development, pp 290\u2013296. Springer, Berlin","DOI":"10.1007\/978-3-319-33600-8_23"},{"key":"314_CR14","series-title":"Texts in theoretical computer science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot Y, Cast\u00e9ran P (2004) Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer, Berlin"},{"key":"314_CR15","unstructured":"Bhattacharyya A (2013) Formal modelling and analysis of dynamic reconfiguration of dependable systems. PhD thesis, Newcastle University School of Computing Science"},{"volume-title":"The Vienna development method: the meta-language. Lecture notes in computer science","year":"1978","key":"314_CR16","unstructured":"Bj\u00f8rner D, Jones CB (eds) (1978) The Vienna development method: the meta-language. Lecture notes in computer science, vol 61. Springer, Berlin"},{"issue":"2","key":"314_CR17","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/s11704-016-5460-3","volume":"12","author":"A Chebieb","year":"2018","unstructured":"Chebieb A, Ait-Ameur Y (2018) A formal model for plastic human computer interfaces. Front Comput Sci 12(2):351\u2013375","journal-title":"Front Comput Sci"},{"key":"314_CR18","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on principles of programming languages, POPL \u201977. ACM, New York, NY, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"314_CR19","doi-asserted-by":"crossref","unstructured":"Diallo N, Ghardallou W, Mili A (2016) Program repair by stepwise correctness enhancement. In: Luca A, Adrian F, Anna I (eds) Proceedings first workshop on pre- and post-deployment verification techniques, PrePost@IFM 2016, Reykjav\u00edk, Iceland, 4th June 2016, EPTCS, vol 208, pp 1\u201315","DOI":"10.4204\/EPTCS.208.1"},{"issue":"2","key":"314_CR20","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1109\/MS.2006.35","volume":"23","author":"R de Lemos","year":"2006","unstructured":"de Lemos R, de Castro Guerra PA, Fischer Rubira CM (2006) A fault-tolerant architectural approach for dependable systems. IEEE Softw 23(2):80\u201387","journal-title":"IEEE Softw"},{"key":"314_CR21","unstructured":"de Palma N, Laumay P, Bellissard L (2001) Ensuring dynamic reconfiguration consistency. In: 6th international workshop on component-oriented programming (WCOP 2001), ECOOP related workshop, pp 18\u201324"},{"key":"314_CR22","series-title":"Texts and monographs in computer science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate calculus and program semantics","author":"EW Dijkstra","year":"1990","unstructured":"Dijkstra EW, Scholten CS (1990) Predicate calculus and program semantics. Texts and monographs in computer science. Springer, Berlin"},{"key":"314_CR23","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, languages and programming","author":"EA Emerson","year":"1980","unstructured":"Emerson EA, Clarke EM (1980) Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker J, van Leeuwen J (eds) Automata, languages and programming, vol 85. Lecture notes in computer science. Springer, Berlin, pp 169\u2013181"},{"issue":"2","key":"314_CR24","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s00165-011-0207-2","volume":"24","author":"A Filieri","year":"2012","unstructured":"Filieri A, Ghezzi C, Tamburrelli G (2012) A formal approach to adaptive software: continuous assurance of non-functional requirements. Form Asp Comput 24(2):163\u2013186","journal-title":"Form Asp Comput"},{"key":"314_CR25","first-page":"9","volume-title":"Specification and validation methods","author":"Y Gurevich","year":"1995","unstructured":"Gurevich Y (1995) Evolving algebras 1993: Lipari guide. In: B\u00f6rger E (ed) Specification and validation methods. Oxford University Press, Oxford, pp 9\u201336"},{"key":"314_CR26","unstructured":"INRIA (2016) The Coq proof assistant reference manual, version 8.5 edition"},{"key":"314_CR27","doi-asserted-by":"crossref","unstructured":"Iftikhar MU, Weyns D (2012) A case study on formal verification of self-adaptive behaviors in a decentralized system. In: Kokash N, Ravara A (eds) 11th international workshop on foundations of coordination languages and self adaptation (FOCLASA\u201912). EPTCS, vol 91, pp 45\u201362","DOI":"10.4204\/EPTCS.91.4"},{"issue":"2","key":"314_CR28","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel M, Butler M (2008) Prob: an automated analysis toolset for the b method. Int J Softw Tools Technol Transf 10(2):185\u2013203","journal-title":"Int J Softw Tools Technol Transf"},{"issue":"2","key":"314_CR29","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.entcs.2011.11.011","volume":"279","author":"A Lanoix","year":"2011","unstructured":"Lanoix A, Dormoy J, Kouchnarenko O (2011) Combining proof and model-checking to validate reconfigurable architectures. Electron Not Theor Comput Sci 279(2):43\u201357 Proceedings of the 8th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA)","journal-title":"Electron Not Theor Comput Sci"},{"issue":"3","key":"314_CR30","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/s11219-013-9208-0","volume":"21","author":"C Le Goues","year":"2013","unstructured":"Le Goues C, Forrest S, Weimer W (2013) Current challenges in automatic software repair. Softw Qual J 21(3):421\u2013443","journal-title":"Softw Qual J"},{"key":"314_CR31","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35813-5_1","volume-title":"Software engineering for self-adaptive systems II","author":"R Lemos","year":"2013","unstructured":"Lemos R, Giese H, M\u00fcller HA, Shaw M, Andersson J, Litoiu M, Schmerl B, Tamura G, Villegas NM, Vogel T, Weyns D, Baresi L, Becker B, Bencomo N, Brun Y, Cukic B, Desmarais R, Dustdar S, Engels G, Geihs K, G\u00f6schka KM, Gorla A, Grassi V, Inverardi P, Karsai G, Kramer J, Lopes A, Magee J, Malek S, Mankovskii S, Mirandola R, Mylopoulos J, Nierstrasz O, Pezz\u00e9 M, Prehofer C, Sch\u00e4fer W, Schlichting R, Smith DB, Sousa JP, Tahvildari L, Wong K, Wuttke J (2013) Software engineering for self-adaptive systems: a second research roadmap. In: Lemos R, Giese H, M\u00fcller HA, Shaw M (eds) Software engineering for self-adaptive systems II, vol 7475. Lecture notes in computer science. Springer, Berlin, pp 1\u201332"},{"issue":"1","key":"314_CR32","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/TSE.2011.104","volume":"38","author":"C Le Goues","year":"2012","unstructured":"Le Goues C, Nguyen TV, Forrest S, Weimer W (2012) Software engineering for self-adaptive systems: a second research roadmap. IEEE Trans Softw Eng 38(1):54\u201372","journal-title":"IEEE Trans Softw Eng"},{"key":"314_CR33","doi-asserted-by":"crossref","unstructured":"Lopatkin I, Romanovsky A (2014) Rigorous development of fault-tolerant systems through co-refinement. Technical report, School of Computing Science, University of Newcastle upon Tyne","DOI":"10.1007\/978-3-319-08311-7_3"},{"key":"314_CR34","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.jss.2013.11.002","volume":"89","author":"R Mirandola","year":"2014","unstructured":"Mirandola R, Potena P, Riccobene E, Scandurra P (2014) A reliability model for service component architectures. J Syst Softw 89:109\u2013127","journal-title":"J Syst Softw"},{"key":"314_CR35","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1016\/j.scico.2013.09.017","volume":"80","author":"R Mirandola","year":"2014","unstructured":"Mirandola R, Potena P, Scandurra P (2014) Adaptation space exploration for service-oriented applications. Sci Comput Program 80:356\u2013384","journal-title":"Sci Comput Program"},{"key":"314_CR36","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014a proof assistant for higher-order logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL\u2014a proof assistant for higher-order logic, vol 2283. Lecture notes in computer science. Springer, Berlin"},{"key":"314_CR37","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11527800_20","volume-title":"Unconventional programming paradigms","author":"M Parashar","year":"2005","unstructured":"Parashar M, Hariri S (2005) Autonomic computing: an overview. In: Ban\u00e2tre J-P, Fradet P, Giavitto J-L, Michel O (eds) Unconventional programming paradigms, vol 3566. Lecture notes in computer science. Springer, Berlin, pp 257\u2013269"},{"issue":"3","key":"314_CR38","doi-asserted-by":"publisher","first-page":"624","DOI":"10.1016\/j.jss.2012.10.929","volume":"86","author":"P Potena","year":"2013","unstructured":"Potena P (2013) Optimization of adaptation plans for a service-oriented architecture with cost, reliability, availability and performance tradeoff. J Syst Softw 86(3):624\u2013648","journal-title":"J Syst Softw"},{"key":"314_CR39","unstructured":"Pereverzeva I, Troubitsyna E, Laibinis L (2012) Development of fault tolerant MAS with cooperative error recovery by refinement in Event-B. In: Ishikawa F, Romanovsky A (eds) DS-Event-B 2012: workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012\u2014Kyoto, Japan, November 13, 2012"},{"issue":"1","key":"314_CR40","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1504\/IJCCBS.2013.053743","volume":"4","author":"I Pereverzeva","year":"2013","unstructured":"Pereverzeva I, Troubitsyna E, Laibinis L (2013) A refinement-based approach to developing critical multi-agent systems. Int J Crit Comput-Based Syst 4(1):69\u201391","journal-title":"Int J Crit Comput-Based Syst"},{"issue":"2","key":"314_CR41","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1109\/TDSC.2010.52","volume":"9","author":"R Rodrigues","year":"2012","unstructured":"Rodrigues R, Liskov B, Chen K, Liskov M, Schultz D (2012) Automatic reconfiguration for large-scale reliable storage systems. IEEE Trans Depend Secure Comput 9(2):145\u2013158","journal-title":"IEEE Trans Depend Secure Comput"},{"key":"314_CR42","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-642-33678-2_18","volume-title":"Computer safety, reliability, and security","author":"A Tarasyuk","year":"2012","unstructured":"Tarasyuk A, Pereverzeva I, Troubitsyna E, Latvala T, Nummila L (2012) Formal development and assessment of a reconfigurable on-board satellite system. In: Ortmeier F, Daniel P (eds) Computer safety, reliability, and security, vol 7612. Lecture notes in computer science. Springer, Berlin, pp 210\u2013222"},{"key":"314_CR43","unstructured":"Wenzel M (2016) The Isabelle\/Isar reference manual"},{"key":"314_CR44","doi-asserted-by":"crossref","unstructured":"Weyns D, Iftikhar MU, de la Iglesia DG, Tanvir A (2012) A survey of formal methods in self-adaptive systems. In: Proceedings of the fifth international c* conference on computer science and software engineering, C3S2E \u201912. ACM, New York, pp 67\u201379","DOI":"10.1145\/2347583.2347592"},{"key":"314_CR45","doi-asserted-by":"crossref","unstructured":"Wermelinger M, Lopes A, Fiadeiro JL (2001) A graph based architectural (re)configuration language. In: Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on foundations of software engineering, ESEC\/FSE-9. ACM, New York, pp 21\u201332","DOI":"10.1145\/503209.503213"}],"container-title":["Service Oriented Computing and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11761-021-00314-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11761-021-00314-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11761-021-00314-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,17]],"date-time":"2021-08-17T16:57:40Z","timestamp":1629219460000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11761-021-00314-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,4]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["314"],"URL":"https:\/\/doi.org\/10.1007\/s11761-021-00314-4","relation":{},"ISSN":["1863-2386","1863-2394"],"issn-type":[{"type":"print","value":"1863-2386"},{"type":"electronic","value":"1863-2394"}],"subject":[],"published":{"date-parts":[[2021,5,4]]},"assertion":[{"value":"5 May 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 October 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 January 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 May 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}