{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T07:27:38Z","timestamp":1761895658505},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,4,2]],"date-time":"2013-04-02T00:00:00Z","timestamp":1364860800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2013,6]]},"DOI":"10.1007\/s11334-013-0204-0","type":"journal-article","created":{"date-parts":[[2013,4,1]],"date-time":"2013-04-01T10:24:41Z","timestamp":1364811881000},"page":"105-117","source":"Crossref","is-referenced-by-count":6,"title":["An experience report on the verification of autonomic protocols in the cloud"],"prefix":"10.1007","volume":"9","author":[{"given":"Gwen","family":"Sala\u00fcn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabienne","family":"Boyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thierry","family":"Coupaye","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noel","family":"De Palma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Etchevers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olivier","family":"Gruber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,4,2]]},"reference":[{"key":"204_CR1","doi-asserted-by":"crossref","unstructured":"Allen R, Douence R, Garlan D (1998) Specifying and analyzing dynamic software architectures. In: Proceedings of FASE\u201998, volume 1382 of LNCS. Springer, Berlin, pp 21\u201337","DOI":"10.1007\/BFb0053581"},{"key":"204_CR2","doi-asserted-by":"crossref","unstructured":"Andova S, Groenewegen L, Stafleu J, de Vink EP (2009) Formalizing adaptation on-the-fly. Electron Notes Theor Comp Sci 255: 23\u201344","DOI":"10.1016\/j.entcs.2009.10.023"},{"issue":"3","key":"204_CR3","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1017\/S0960129504004153","volume":"14","author":"F Arbab","year":"2004","unstructured":"Arbab F (2004) Reo: a channel-based coordination model for component composition. Math Struct Comp Sci 14(3):329\u2013366","journal-title":"Math Struct Comp Sci"},{"issue":"1\u20132","key":"204_CR4","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/s12243-008-0069-7","volume":"64","author":"T Barros","year":"2009","unstructured":"Barros T, Ameur-Boulifa R, Cansado A, Henrio L, Madelaine E (2009) Behavioural models for distributed fractal components. Ann des T\u00e9l\u00e9commun 64(1\u20132):25\u201343","journal-title":"Ann des T\u00e9l\u00e9commun"},{"key":"204_CR5","doi-asserted-by":"crossref","unstructured":"Bellissard L, De Palma N, Freyssinet A, Herrmann M, Lacourte S (1999) An agent platform for reliable asynchronous distributed programming. In: Proceedings of SRDS\u201999, IEEE Computer Society, pp 294\u2013295","DOI":"10.1109\/RELDIS.1999.805107"},{"key":"204_CR6","doi-asserted-by":"crossref","unstructured":"Bergamini D, Descoubes N, Joubert C, Mateescu R (2005) BISIMULATOR: a modular tool for on-the-fly equivalence checking. In: Proceedings of TACAS\u201905, volume 3440 of LNCS, Springer, Berlin, pp 581\u2013585","DOI":"10.1007\/978-3-540-31980-1_42"},{"key":"204_CR7","doi-asserted-by":"crossref","unstructured":"Bernot G, Gaudel M-C, Marre B (1991) Software testing vased on formal specifications: a theory and a tool. Softw Eng J 6(6): 387\u2013405","DOI":"10.1049\/sej.1991.0040"},{"key":"204_CR8","doi-asserted-by":"crossref","unstructured":"Boyer F, Gruber O, Sala\u00fcn G (2011) Specifying and verifying the synergy reconfiguration protocol with LOTOS NT and CADP. In: Proceedings of FM\u201911, volume 6664 of LNCS, Springer, Berlin, pp 103\u2013117","DOI":"10.1007\/978-3-642-21437-0_10"},{"key":"204_CR9","doi-asserted-by":"crossref","unstructured":"Bozzano M, Cimatti A, Katoen J-P, Nguyen VY, Noll T, Roveri M, Wimmer R (2010) A model checker for AADL. In: Proceedings of CAV\u201910, volume 6174 of LNCS, Springer, Berlin, pp 562\u2013565","DOI":"10.1007\/978-3-642-14295-6_48"},{"key":"204_CR10","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/j.entcs.2010.05.006","volume":"263","author":"A Cansado","year":"2010","unstructured":"Cansado A, Canal C, Sala\u00fcn G, Cubo J (2010) A formal framework for structural reconfiguration of components under behavioural adaptation. Electron Notes Theor Comput Sci 263:95\u2013110","journal-title":"Electron Notes Theor Comput Sci"},{"key":"204_CR11","unstructured":"Champelovier D, Clerc X, Garavel H, Guerte Y, Powazny V, Lang F, Serwe W, Smeding G (2011) Reference manual of the LOTOS NT to LOTOS translator (Version 5.4), INRIA\/VASY"},{"key":"204_CR12","doi-asserted-by":"crossref","unstructured":"Chapman C, Emmerich W, Gal\u00e1n M\u00e1rquez F, Clayman S, Galis A (2010) Software architecture definition for on-demand cloud provisioning. In: Proceedings of HPDC\u201910, ACM Press, pp 61\u201372","DOI":"10.1145\/1851476.1851485"},{"key":"204_CR13","unstructured":"Cornejo MA, Garavel H, Mateescu R, De Palma N (2001) Specification and verification of a dynamic reconfiguration protocol for agent-based applications. In: Proceedings of DAIS\u201901, volume 198 of IFIP Conference Proceedings, Kluwer, pp 229\u2013244"},{"key":"204_CR14","doi-asserted-by":"crossref","unstructured":"Crouzen P, Lang F (2011) Smart reduction. In: Proceedings of FASE\u201911, volume 6603 of LNCS, Springer, Berlin, pp 111\u2013126.","DOI":"10.1007\/978-3-642-19811-3_9"},{"key":"204_CR15","doi-asserted-by":"crossref","unstructured":"Etchevers X, Coupaye T, Boyer F, de Palma N (2011) Self-configuration of distributed applications in the cloud. In: Proceedings of CLOUD\u201911, IEEE Computer Society, pp 668\u2013675","DOI":"10.1109\/CLOUD.2011.65"},{"key":"204_CR16","doi-asserted-by":"crossref","unstructured":"Furht B, Escalante A (eds) (2010) Handbook of cloud computing. Springer, Berlin","DOI":"10.1007\/978-1-4419-6524-0"},{"key":"204_CR17","doi-asserted-by":"crossref","unstructured":"Garavel H, Lang F, Mateescu R, Serwe W (2011) CADP 2010: a toolbox for the construction and analysis of distributed processes. In: Proceedings of TACAS\u201911, volume 6605 of LNCS, Springer, Berlin, pp 372\u2013387","DOI":"10.1007\/978-3-642-19835-9_33"},{"key":"204_CR18","unstructured":"Garavel H, Mateescu R, Serwe W (2012) Large-scale distributed verification using CADP: beyond clusters to grids. In: Proceedings of PDMC\u201912"},{"key":"204_CR19","doi-asserted-by":"crossref","unstructured":"Garavel H, Sighireanu M (1999) A graphical parallel composition operator for process algebras. In: Proceedings of FORTE\u201999, volume 156 of IFIP conference proceedings, Kluwer, pp 185\u2013202","DOI":"10.1007\/978-0-387-35578-8_11"},{"issue":"3","key":"204_CR20","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1007\/s100090100044","volume":"3","author":"H Garavel","year":"2001","unstructured":"Garavel H, Viho C, Zendri M (2001) System design of a CC-NUMA multiprocessor architecture using formal specification, model checking, co-simulation, and test generation. STTT 3(3):314\u2013331","journal-title":"STTT"},{"issue":"1","key":"204_CR21","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1145\/1496909.1496915","volume":"43","author":"P Goldsack","year":"2009","unstructured":"Goldsack P, Guijarro J, Loughran S, Coles A, Farrell A, Lain A, Murray P, Toft P (2009) The SmartFrog configuration management framework. SIGOPS Oper Syst Rev 43(1):16\u201325","journal-title":"SIGOPS Oper Syst Rev"},{"key":"204_CR22","unstructured":"ISO\/IEC (2001) Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization, Information Technology"},{"key":"204_CR23","doi-asserted-by":"crossref","unstructured":"Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2009) seL4: formal verification of an OS Kernel. In: Proceedings of SOSP\u201909, ACM Press, pp 207\u2013220","DOI":"10.1145\/1629575.1629596"},{"issue":"11","key":"204_CR24","first-page":"1293","volume":"16","author":"J Kramer","year":"1990","unstructured":"Kramer J, Magee J (1990) The evolving philosophers problem: dynamic change management. IEEE TSE 16(11):1293\u20131306","journal-title":"IEEE TSE"},{"issue":"5","key":"204_CR25","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1049\/ip-sen:19982297","volume":"145","author":"J Kramer","year":"1998","unstructured":"Kramer J, Magee J (1998) Analysing dynamic change in distributed software architectures. IEE Proc Softw 145(5):146\u2013154","journal-title":"IEE Proc Softw"},{"issue":"1","key":"204_CR26","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.scico.2009.10.006","volume":"76","author":"C Krause","year":"2011","unstructured":"Krause C, Maraikar Z, Lazovik A, Arbab F (2011) Modeling dynamic reconfigurations in Reo using high-level replacement systems. Sci Comp Programm 76(1):23\u201336","journal-title":"Sci Comp Programm"},{"key":"204_CR27","doi-asserted-by":"crossref","unstructured":"Lantreibecq E, Serwe W (2011) Model checking and co-simulation of a dynamic task dispatcher circuit using CADP. In: Proceedings of FMICS\u201911, volume 6959 of LNCS, Springer, pp 180\u2013195","DOI":"10.1007\/978-3-642-24431-5_14"},{"key":"204_CR28","doi-asserted-by":"crossref","unstructured":"Magee J, Kramer J, Giannakopoulou D (1999) Behaviour analysis of software architectures. In: Proceedings of WICSA\u201999, volume 140 of IFIP conference proceedings, Kluwer, pp 35\u201350","DOI":"10.1007\/978-0-387-35563-4_3"},{"key":"204_CR29","doi-asserted-by":"crossref","unstructured":"Mateescu R, Thivolle D (2008) A model checking language for concurrent value-passing systems. In: Proceedings of FM\u201908, volume 5014 of LNCS, Springer, pp 148\u2013164","DOI":"10.1007\/978-3-540-68237-0_12"},{"key":"204_CR30","unstructured":"Mirkovic J, Faber T, Hsieh P, Malayandisamu G, Malavia R (2010) DADL: distributed application description language. USC\/ISI Technical, Report ISI-TR-664"},{"key":"204_CR31","doi-asserted-by":"crossref","unstructured":"Sala\u00fcn G, Etchevers X, De Palma N, Boyer F, Coupaye T (2012) Verification of a self-configuration protocol for distributed applications in the cloud. In: Proceedings of SAC\u201912, ACM Press, pp 1278\u20131283","DOI":"10.1145\/2245276.2231979"},{"key":"204_CR32","volume-title":"Agile project management with scrum","author":"K Schwaber","year":"2004","unstructured":"Schwaber K (2004) Agile project management with scrum. Microsoft Press, Redmond"},{"key":"204_CR33","unstructured":"Vassev E, Hinchey M, Quigley A (2009) Model checking for autonomic systems specified with ASSL. In: Proceedings of NFM\u201909, pp 16\u201325"},{"key":"204_CR34","doi-asserted-by":"crossref","unstructured":"Wermelinger M, Lopes A, Fiadeiro JL (2001) A graph based architectural (Re)configuration language. In: Proceedings of ESEC\/SIGSOFT FSE\u201901, ACM Press, pp 21\u201332","DOI":"10.1145\/503209.503213"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-013-0204-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-013-0204-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-013-0204-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,24]],"date-time":"2020-07-24T17:00:03Z","timestamp":1595610003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-013-0204-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,2]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["204"],"URL":"https:\/\/doi.org\/10.1007\/s11334-013-0204-0","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4,2]]}}}