{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T18:10:03Z","timestamp":1749924603106,"version":"3.41.0"},"reference-count":101,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T00:00:00Z","timestamp":1488326400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000774","name":"Newcastle University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000774","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper uses a case study to evaluate empirically three formalisms of different kinds for their suitability for the modelling and analysis of dynamic reconfiguration of dependable systems. The requirements on an ideal formalism for dynamic software reconfiguration are defined. The reconfiguration of an office workflow for order processing is described, and the requirements on the reconfiguration of the workflow are defined. The workflow is modelled using the Vienna Development Method (VDM), conditional partial order graphs (CPOGs), and the basic Calculus of Communicating Systems for dynamic process reconfiguration (basic CCS<jats:sup>dp<\/jats:sup>), and verification of the reconfiguration requirements is attempted using the models. The formalisms are evaluated according to their ability to model the reconfiguration of the workflow, to verify the requirements on the workflow\u2019s reconfiguration, and to meet the requirements on an ideal formalism.<\/jats:p>","DOI":"10.1007\/s00165-016-0405-z","type":"journal-article","created":{"date-parts":[[2017,1,20]],"date-time":"2017-01-20T12:02:55Z","timestamp":1484913775000},"page":"251-307","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems"],"prefix":"10.1145","volume":"29","author":[{"given":"Anirban","family":"Bhattacharyya","sequence":"first","affiliation":[{"name":"School of Computing Science, Newcastle University, Claremont Tower, Claremont Road, NE1 7RU, Newcastle upon Tyne, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrey","family":"Mokhov","sequence":"additional","affiliation":[{"name":"School of Electrical and Electronic Engineering, Newcastle University, Merz Court, NE1 7RU, Newcastle upon Tyne, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ken","family":"Pierce","sequence":"additional","affiliation":[{"name":"School of Computing Science, Newcastle University, Claremont Tower, Claremont Road, NE1 7RU, Newcastle upon Tyne, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.11.034"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Agerholm S Lecoeur P-J Reichert E (1998) Formal specification and validation at work: a case study using VDM-SL. In: Proceedings of the second workshop on formal methods in software practice FMSP \u201998 pp 78\u201384 New York NY USA ACM","DOI":"10.1145\/298595.298861"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Aguirre N Maibaum T (2002) A temporal logic approach to the specification of reconfigurable component-based systems. In: Proceedings of the 17th IEEE international conference on automated software engineering pp 271\u2013274","DOI":"10.1109\/ASE.2002.1115028"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.1011"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Almeida JPA Wegdam M van Sinderen M Nieuwenhuis L (2001) Transparent dynamic reconfiguration for CORBA. In: Proceedings of the 3rd international symposium on distributed objects and applications pp 197\u2013207","DOI":"10.1109\/DOA.2001.954085"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90185-I"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Boreale M Bruni R Caires L De Nicola R Lanese I. Loreti M Martins F Montanari U Ravara A Sangiorgi D Vasconcelos V Zavattaro G (2006) SCC: a service centered calculus. In: Proceedings of the 3rd international workshop on web services and formal methods (WS-FM) pp 38\u201357","DOI":"10.1007\/11841197_3"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Bradbury JS Cordy JR Dingel J Wermelinger M (2004) A survey of self-management in dynamic software architecture specifications. In: Proceedings of the 1st ACM SIGSOFT workshop on self-managed systems pp 28\u201333","DOI":"10.1145\/1075405.1075411"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1993.0014"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Bicarregui J Fitzgerald J Lindsay P Moore R Ritchie B (1994) Proof in VDM: a practitioner\u2019s guide. FACIT. Springer-Verlag. ISBN 3-540-19813-X","DOI":"10.1007\/978-1-4471-2033-9"},{"key":"e_1_2_1_2_11_2","unstructured":"Bhattacharyya A (2013) Formal modelling and analysis of dynamic reconfiguration of dependable systems. PhD thesis Newcastle University School of Computing Science. http:\/\/hdl.handle.net\/10443\/1851."},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Butler M Hoare T Ferreira C (2005) A trace semantics for long-running transactions. In: Proceedings of the symposium on the occasion of 25\u00a0years of CSP pp 133\u2013150","DOI":"10.1007\/11423348_8"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80025-X"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Bocchi L Laneve C Zavattaro G (2003) A calculus for long-running transactions. In: Proceedings of the 6th IFIP WG 6.1 international conference on formal methods for open object-based distributed systems (FMOODS) pp 124\u2013138","DOI":"10.1007\/978-3-540-39958-2_9"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90044-E"},{"key":"e_1_2_1_2_16_2","unstructured":"Boudol G (1992) Asynchrony and the \u03c0-calculus. Technical report 1702. Institut National de Recherche en Informatique et en Automatique"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Bravetti M (2002) Specification and analysis of stochastic real-time systems. PhD thesis University of Bologna","DOI":"10.1007\/3-540-45605-8_14"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Bradfield J Stirling C (2007) Handbook of modal logic chapter Modal mu-calculi. Elsevier Science Inc New York NY pp 721\u2013756","DOI":"10.1016\/S1570-2464(07)80015-2"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/37.4.233"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2010.139"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Classen A Heymans P Schobbens P-Y Legay A Raskin J-F (2010) Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd ACM\/IEEE international conference on software engineering ACM vol 1 pp 335\u2013344","DOI":"10.1145\/1806799.1806850"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm030"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1049\/ip-sen:20010558"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Ellis C Keddara K Rozenberg G (1995) Dynamic change within workflow systems. In: Proceedings of the conference on organizational computing systems ACM pp 10\u201321","DOI":"10.1145\/224019.224021"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Ehrig H Pfender M Schneider HJ (1973) Graph-grammars: an algebraic approach. In: IEEE conference record of the 14th annual symposium on switching and automata theory pp 167\u2013180","DOI":"10.1109\/SWAT.1973.11"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"E\u00e9n N S\u00f6rensson N (2004) An extensible SAT-solver. Theory and applications of satisfiability testing pp 333\u2013336","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"e_1_2_1_2_27_2","unstructured":"Endler M Wei J (1992) Programming generic dynamic reconfigurations for distributed applications. In: Proceedings of the international workshop on configurable distributed systems IET pp 68\u201379"},{"issue":"3","key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1145\/2211616.2211619","article-title":"A logical verification methodology for service-oriented computing","volume":"21","author":"Fantechi A","year":"2012","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Filieri A Hoffmann H Maggio M (2015) Automated multi-objective control for self-adaptive software design. In: Proceedings of the 10th joint meeting on foundations of software engineering pp 13\u201324","DOI":"10.1145\/2786805.2786833"},{"key":"e_1_2_1_2_30_2","unstructured":"Fitzgerald J Larsen PG (2009) Modelling systems\u2014practical tools and techniques in software development 2nd edn. Cambridge University Press The Edinburgh Building Cambridge CB2 2RU UK. ISBN 0-521-62348-0."},{"key":"e_1_2_1_2_31_2","unstructured":"Fitzgerald J Larsen PG Mukherjee P Plat N Verhoef M (2005) Validated designs for object-oriented systems. Springer New York"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1361213.1361214"},{"key":"e_1_2_1_2_33_2","unstructured":"F\u0103rca\u015f E (2006) Scheduling multi-mode real-time distributed components. PhD thesis University of Salzburg Department of Computer Sciences"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Fischmeister S Winkler K (2005) Non-blocking deterministic replacement of functionality timing and data-flow for hard real-time systems at runtime. In: Proceedings of the 17th Euromicro conference on real-time systems pp 106\u2013114. IEEE Computer Society","DOI":"10.1109\/ECRTS.2005.20"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Guidi C Lucchi R Gorrieri R Busi N Zavattaro G (2006) SOCK: a calculus for service oriented computing. In: Proceedings of the 4th international conference on service-oriented computing (ICSOC) pp 327\u2013338","DOI":"10.1007\/11948148_27"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Hilario M Nguyen P Do H Woznica A Kalousis A (2011) Ontology-based meta-mining of knowledge discovery workflows. In: Jankowski N Duch W Gra\u0327bczewski K (eds) Meta-learning in computational intelligence volume 358 of Studies in computational intelligence. Springer pp 273\u2013315","DOI":"10.1007\/978-3-642-20980-2_9"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Honda K Tokoro M (1991) An object calculus for asynchronous communication. In: Proceedings of the 5th European conference on object-oriented programming (ECOOP) pp 133\u2013147","DOI":"10.1007\/BFb0057019"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/242224.242477"},{"key":"e_1_2_1_2_39_2","unstructured":"Andrews DJ (1996) Information technology\u2014programming languages their environments and system software interfaces\u2014Vienna Development Method\u2014specification language\u2014part 1: base language"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.385973"},{"key":"e_1_2_1_2_41_2","unstructured":"Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis Oxford University"},{"key":"e_1_2_1_2_42_2","unstructured":"Jones CB (1990) Systematic software development using VDM 2nd edn. Prentice-Hall Inc. Upper Saddle River NJ"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.2003.1203057"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Kaplan SM Goering SK Campbell RH (1989) Specifying concurrent systems with \u0394-grammars. In: Proceedings of the 5th international workshop on software specification and design pp 20\u201327","DOI":"10.1145\/75200.75203"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Kaplan SM Kaiser GE (1988) Garp: graph abstractions for concurrent programming. In: Proceedings of the 2nd European symposium on programming pp 191\u2013205","DOI":"10.1007\/3-540-19027-9_13"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.60317"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2009.10.006"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2010.135"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Kobayashi N (2006) A new type system for deadlock-free processes. In: Proceedings of the 17th international conference on concurrency theory (CONCUR) pp 233\u2013247. Springer-Verlag","DOI":"10.1007\/11817949_16"},{"issue":"8","key":"e_1_2_1_2_50_2","first-page":"692","article-title":"Ten years of historical development: \u201cBootstrapping\u201d VDMTools","volume":"7","author":"Larsen PG","year":"2001","journal-title":"J Univers Comput Sci"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/1668862.1668864"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Lausdahl K Coleman JW Larsen PG (2013) Semantics of the VDM real-time dialect. Technical report ECE-TR-13 Aarhus University","DOI":"10.7146\/ece.v2i13.21228"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1959.tb01585.x"},{"issue":"2","key":"e_1_2_1_2_54_2","first-page":"305","article-title":"Methods for the development of distributed real-time embedded systems using VDM","volume":"3","author":"Larsen PG","year":"2009","journal-title":"Int J Softw Inform"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Larsen PG Lausdahl K Battle N (2010) Combinatorial testing for VDM. In: Proceedings of the 8th IEEE international conference on software engineering and formal methods SEFM \u201910 pp 278\u2013285 Washington DC USA September 2010. IEEE Computer Society. ISBN 978-0-7695-4153-2.","DOI":"10.1109\/SEFM.2010.32"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2006.05.007"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Lin H-H Omori Y Kusakabe S Araki K (2016) Towards verifying VDM using SPIN. In: Proceedings of the 4th international workshop on formal techniques for safety-critical systems volume 596 of Communications in computer and information science pp 241\u2013256. Springer","DOI":"10.1007\/978-3-319-29510-7_14"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.1016\/0920-5489(95)00026-Q"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Mazzara M Abouzaid F Dragoni N Bhattacharyya A (2012) Toward design modelling and analysis of dynamic workflow reconfiguration\u2014a process algebra perspective. In: Proceedings of the 8th international workshop on web services and formal method (WS-FM) volume 7176 of Lecture notes in computer science pp 64\u201378. Springer-Verlag","DOI":"10.1007\/978-3-642-29834-9_6"},{"key":"e_1_2_1_2_60_2","unstructured":"The Maude System (2015) http:\/\/maude.cs.uiuc.edu. Accessed 4 Aug 2016."},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Mazzara M (2006) Towards abstractions for web services composition. PhD thesis University of Bologna Department of Computer Science","DOI":"10.1007\/11841197_17"},{"issue":"172","key":"e_1_2_1_2_62_2","first-page":"8581","article-title":"LTL-based verification of reconfigurable workflows","volume":"8","author":"Mazzara M","year":"2014","journal-title":"Appl Math Sci"},{"key":"e_1_2_1_2_63_2","doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: von Bochmann G Probst D (eds) Computer aided verification. Springer pp 164\u2013177","DOI":"10.1007\/3-540-56496-9_14"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"crossref","unstructured":"Le Metayer D (1996) Software architecture styles as graph grammars. In: Proceedings of the 4th symposium on the foundations of software engineering pp 15\u201323","DOI":"10.1145\/250707.239105"},{"key":"e_1_2_1_2_65_2","unstructured":"Milner R (1989) Communication and concurrency. Prentice-Hall Inc. Upper Saddle River NJ"},{"key":"e_1_2_1_2_66_2","unstructured":"Milner R (1999) Communicating and mobile systems: the \u03c0-calculus. Cambridge University Press Cambridge"},{"key":"e_1_2_1_2_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/2627351"},{"key":"e_1_2_1_2_68_2","doi-asserted-by":"publisher","DOI":"10.5555\/1662594.1662602"},{"key":"e_1_2_1_2_69_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2010.136"},{"key":"e_1_2_1_2_70_2","doi-asserted-by":"crossref","unstructured":"Mokhov A (2009) Conditional partial order graphs. PhD thesis Newcastle University","DOI":"10.1109\/ACSD.2008.4574604"},{"key":"e_1_2_1_2_71_2","doi-asserted-by":"publisher","DOI":"10.1023\/B:TIME.0000027932.11280.3c"},{"key":"e_1_2_1_2_72_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_2_73_2","doi-asserted-by":"publisher","DOI":"10.3390\/jlpea4010026"},{"key":"e_1_2_1_2_74_2","doi-asserted-by":"crossref","unstructured":"Mokhov A Sokolov D Yakovlev A (2012) Adapting asynchronous circuits to operating conditions by logic parametrisation. In: IEEE international symposium on asynchronous circuits and systems (ASYNC) IEEE pp 17\u201324","DOI":"10.1109\/ASYNC.2012.23"},{"key":"e_1_2_1_2_75_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.825767"},{"key":"e_1_2_1_2_76_2","doi-asserted-by":"crossref","unstructured":"Mokhov A Yakovlev A (2008) Verification of conditional partial order graphs. In: International conference on application of concurrency to system design (ACSD) IEEE pp 128\u2013137","DOI":"10.1109\/ACSD.2008.4574604"},{"key":"e_1_2_1_2_77_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.58"},{"key":"e_1_2_1_2_78_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90112-2"},{"key":"e_1_2_1_2_79_2","unstructured":"Oreizy P (1998) Issues in modeling and analyzing dynamic software architectures. In: Proceedings of the international workshop on the role of software architecture in testing and analysis pp 54\u201357"},{"key":"e_1_2_1_2_80_2","doi-asserted-by":"crossref","unstructured":"Patikirikorala T Colman A Han J Wang L (2012) A systematic survey on the design of self-adaptive software systems using control engineering approaches. In: Proceedings of the 7th international symposium on software engineering for adaptive and self-managing systems pp 33\u201342","DOI":"10.1109\/SEAMS.2012.6224389"},{"key":"e_1_2_1_2_81_2","unstructured":"Pedro PSM (1999) Schedulability of mode changes in flexible real-time distributed systems. PhD thesis University of York Department of Computer Science"},{"key":"e_1_2_1_2_82_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE annual symposium on foundations of computer science pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_83_2","doi-asserted-by":"crossref","unstructured":"Pierce BC Turner DN (2000) Pict: a programming language based on the pi-calculus. In: Plotkin G Stirling C Tofte M (eds) Proof language and interaction: essays in honour of Robin Milner. MIT Press Cambridge MA pp 455\u2013494","DOI":"10.7551\/mitpress\/5641.003.0022"},{"key":"e_1_2_1_2_84_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2011.11.002"},{"key":"e_1_2_1_2_85_2","doi-asserted-by":"crossref","unstructured":"Parrow J Victor B (1998) The fusion calculus: expressiveness and symmetry in mobile processes. In: Proceedings of the 13th annual IEEE symposium on logic in computer science pp 176\u2013185","DOI":"10.1109\/LICS.1998.705654"},{"key":"e_1_2_1_2_86_2","doi-asserted-by":"crossref","unstructured":"Rensink A (2003) The GROOVE simulator: a tool for state space generation. In: Pfaltz JL Nagl M B\u00f6hlen B (eds) Applications of graph transformations with industrial relevance. Springer pp 479\u2013485","DOI":"10.1007\/978-3-540-25959-6_40"},{"key":"e_1_2_1_2_87_2","doi-asserted-by":"crossref","unstructured":"Rounds WC Song H (2003) The \u03a6-calculus: a language for distributed control of reconfigurable embedded systems. In: Proceedings of the 6th international workshop on hybrid systems: computation and control pp 435\u2013449","DOI":"10.1007\/3-540-36580-X_32"},{"key":"e_1_2_1_2_88_2","unstructured":"Sangiorgi D (1993) Expressing mobility in process algebras: first-order and higher-order paradigms. PhD thesis University of Edinburgh Department of Computer Science"},{"key":"e_1_2_1_2_89_2","unstructured":"SEN3. The Reo Project (2008). http:\/\/reo.project.cwi.nl\/reo\/wiki. Accessed 4 Aug 2016"},{"key":"e_1_2_1_2_90_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00365439"},{"key":"e_1_2_1_2_91_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.637390"},{"key":"e_1_2_1_2_92_2","doi-asserted-by":"crossref","DOI":"10.1017\/9781316134924","volume-title":"The \u03c0-calculus: a theory of mobile processes","author":"Sangiorgi D","year":"2001"},{"key":"e_1_2_1_2_93_2","doi-asserted-by":"crossref","unstructured":"Taentzer G (2003) AGG: a graph transformation environment for modeling and validation of software. In: Pfaltz JL Nagl M B\u00f6hlen B (eds) Applications of graph transformations with industrial relevance. Springer pp 446\u2013453","DOI":"10.1007\/978-3-540-25959-6_35"},{"key":"e_1_2_1_2_94_2","doi-asserted-by":"crossref","unstructured":"Tindell K Burns A Wellings A (1992) Mode changes in priority pre-emptively scheduled systems. In: Proceedings of the IEEE real-time systems symposium pp100\u2013109","DOI":"10.1109\/REAL.1992.242672"},{"key":"e_1_2_1_2_95_2","unstructured":"Thomsen B (1990) Calculi for higher order communicating systems. PhD thesis University of London Imperial College of Science Technology and Medicine Department of Computing"},{"key":"e_1_2_1_2_96_2","doi-asserted-by":"crossref","unstructured":"Verhoef M Larsen PG Hooman J (2006) Modeling and validating distributed embedded real-time systems with VDM++. In: Misra J Nipkow T Sekerinski E (eds) FM 2006: formal methods. Lecture notes in computer science vol. 4085. Springer Berlin pp 147\u2013162","DOI":"10.1007\/11813040_11"},{"key":"e_1_2_1_2_97_2","doi-asserted-by":"crossref","unstructured":"Victor B Moller F (1994) The mobility workbench\u2014a tool for the \u03c0-calculus. In: Proceedings of the 6th international conference on computer aided verification pp 428\u2013440. Springer-Verlag","DOI":"10.1007\/3-540-58179-0_73"},{"key":"e_1_2_1_2_98_2","doi-asserted-by":"crossref","unstructured":"Wermelinger MA (1999) Specification of software architecture reconfiguration. PhD thesis University of Lisbon Department of Informatics","DOI":"10.1145\/318774.319256"},{"key":"e_1_2_1_2_99_2","doi-asserted-by":"crossref","unstructured":"Weyns D Iftikhar MU de la Iglesia DG Ahmad T (2012) A survey of formal methods in self-adaptive systems. In: Proceedings of the 5th international C* conference on computer science and software engineering pp 67\u201379","DOI":"10.1145\/2347583.2347592"},{"key":"e_1_2_1_2_100_2","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503213"},{"key":"e_1_2_1_2_101_2","unstructured":"Yu T Lin KJ (2005) Adaptive algorithms for finding replacement services in autonomic distributed business processes. In: Proceedings of the 7th international symposium on autonomous decentralized systems IEEE pp 427\u2013434"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0405-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0405-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0405-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0405-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T17:52:07Z","timestamp":1749923527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0405-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3]]},"references-count":101,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["10.1007\/s00165-016-0405-z"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0405-z","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,3]]}}}