An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems
Pages 251 - 307
Abstract
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 CCSdp), 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’s reconfiguration, and to meet the requirements on an ideal formalism.
References
References
[1]
Andova S, Groenewegen LPJ, and de Vink EP Dynamic adaptation with distributed control in Paradigm Sci Comput Program 2014 94 333-361
[2]
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 ’98, pp 78–84, New York, NY, USA, ACM
[3]
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–274
[4]
Ardagna D and Pernici B Adaptive service composition in flexible processes IEEE Trans Softw Eng 2007 33 6 369-384
[5]
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–207
[6]
Berry G and Boudol G The chemical abstract machine Theor Comput Sci 1992 96 1 217-248
[7]
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–57
[8]
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–33
[9]
Bloom T and Day M Reconfiguration and module replacement in Argus: theory and practice Softw Eng J (Special Issue) 1993 8 2 102-108
[10]
Bicarregui J, Fitzgerald J, Lindsay P, Moore R, Ritchie B (1994) Proof in VDM: a practitioner’s guide. FACIT. Springer-Verlag. ISBN 3-540-19813-X
[11]
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.
[12]
Butler M, Hoare T, Ferreira C (2005) A trace semantics for long-running transactions. In: Proceedings of the symposium on the occasion of 25 years of CSP, pp 133–150
[13]
Bergstra JA and Klop JW Process algebra for synchronous communication Inf Control 1984 60 109-137
[14]
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–138
[15]
Banâtre JP and Le Métayer D The GAMMA model and its discipline of programming Sci Comput Program 1990 15 1 55-77
[16]
Boudol G (1992) Asynchrony and the π-calculus. Technical report 1702. Institut National de Recherche en Informatique et en Automatique
[17]
Bravetti M (2002) Specification and analysis of stochastic real-time systems. PhD thesis, University of Bologna
[18]
Bradfield J, Stirling C (2007) Handbook of modal logic, chapter Modal mu-calculi. Elsevier Science Inc, New York, NY, pp 721–756
[19]
Christensen S, Hirshfeld Y, and Moller F Decidable subsets of CCS Comput J 1994 37 4 233-242
[20]
Coyle L, Hinchey M, Nuseibeh B, and Fiadeiro JL Guest Editors’ introduction: evolving critical systems IEEE Comput 2010 43 5 28-33
[21]
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–344
[22]
Coleman JW and Jones CB A structural proof of the soundness of rely/guarantee rules J Log Comput 2007 17 807-841
[23]
Cho SM, Kim HH, Cha SD, and Bae DH Specification and validation of dynamic systems using temporal logic IEE Proc Softw 2001 148 4 135-140
[24]
Ellis C, Keddara K, Rozenberg G (1995) Dynamic change within workflow systems. In: Proceedings of the conference on organizational computing systems, ACM, pp 10–21
[25]
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–180
[26]
Eén N, Sörensson N (2004) An extensible SAT-solver. Theory and applications of satisfiability testing, pp 333–336
[27]
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–79
[28]
Fantechi A, Gnesi S, Lapadula A, Mazzanti F, Pugliese R, and Tiezzi F A logical verification methodology for service-oriented computing ACM Trans Softw Eng Methodol 2012 21 3 16-11646
[29]
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–24
[30]
Fitzgerald J, Larsen PG (2009) Modelling systems—practical tools and techniques in software development, 2nd edn. Cambridge University Press, The Edinburgh Building, Cambridge CB2 2RU, UK. ISBN 0-521-62348-0.
[31]
Fitzgerald J, Larsen PG, Mukherjee P, Plat N, Verhoef M (2005) Validated designs for object-oriented systems. Springer, New York
[32]
Fitzgerald J, Larsen PG, and Sahara S VDMTools: advances in support for formal modeling in VDM ACM Sigplan Not 2008 43 2 3-11
[33]
Fărcaş E (2006) Scheduling multi-mode real-time distributed components. PhD thesis, University of Salzburg Department of Computer Sciences
[34]
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–114. IEEE Computer Society
[35]
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–338
[36]
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̧bczewski K (eds) Meta-learning in computational intelligence, volume 358 of Studies in computational intelligence. Springer, pp 273–315
[37]
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–147
[38]
Hudak P Building domain-specific embedded languages ACM Comput Surv 1996 28 4 196
[39]
Andrews DJ (1996) Information technology—programming languages, their environments and system software interfaces—Vienna Development Method—specification language—part 1: base language
[40]
Inverardi P and Wolf AL Formal specification and analysis of software architectures using the chemical abstract machine model IEEE Trans Softw Eng 1995 21 4 373-386
[41]
Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis, Oxford University
[42]
Jones CB (1990) Systematic software development using VDM, 2nd edn. Prentice-Hall, Inc., Upper Saddle River, NJ
[43]
Jones CB The early search for tractable ways of reasonning about programs IEEE Ann Hist Comput 2003 25 2 26-49
[44]
Kaplan SM, Goering SK, Campbell RH (1989) Specifying concurrent systems with Δ-grammars. In: Proceedings of the 5th international workshop on software specification and design, pp 20–27
[45]
Kaplan SM, Kaiser GE (1988) Garp: graph abstractions for concurrent programming. In: Proceedings of the 2nd European symposium on programming, pp 191–205
[46]
Kramer J and Magee J The evolving philosophers problem: dynamic change management IEEE Trans Softw Eng 1990 16 11 1293-1306
[47]
Krause C, Maraikar Z, Lazovik A, and Arbab F Modeling dynamic reconfigurations in Reo using high-level replacement systems Sci Comput Program 2011 76 23-36
[48]
Karsai G, Massacci F, Osterweil LJ, and Schieferdecker I Evolving embedded systems IEEE Comput 2010 43 5 34-40
[49]
Kobayashi N (2006) A new type system for deadlock-free processes. In: Proceedings of the 17th international conference on concurrency theory (CONCUR), pp 233–247. Springer-Verlag
[50]
Larsen PG Ten years of historical development: “Bootstrapping” VDMTools J Univers Comput Sci 2001 7 8 692-709
[51]
Larsen PG, Battle N, Ferreira M, Fitzgerald J, Lausdahl K, and Verhoef M The overture initiative-integrating tools for VDM SIGSOFT Softw Eng Notes 2010 35 1 1-6
[52]
Lausdahl K, Coleman JW, Larsen PG (2013) Semantics of the VDM real-time dialect. Technical report ECE-TR-13, Aarhus University
[53]
Lee C-Y Representation of switching circuits by binary-decision programs Bell Syst Tech J 1959 38 4 985-999
[54]
Larsen PG, Fitzgerald J, and Wolff S Methods for the development of distributed real-time embedded systems using VDM Int J Softw Inform 2009 3 2–3 305-341
[55]
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 ’10, pp 278–285, Washington, DC, USA, September 2010. IEEE Computer Society. ISBN 978-0-7695-4153-2.
[56]
Lucchi R and Mazzara M A pi-calculus based semantics for WS-BPEL J Log Algebr Program 2007 70 1 96-118
[57]
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–256. Springer
[58]
Larsen PG and Pawłowski W The formal semantics of ISO VDM-SL Comput Stand Interfaces 1995 17 5–6 585-602
[59]
Mazzara M, Abouzaid F, Dragoni N, Bhattacharyya A (2012) Toward design, modelling and analysis of dynamic workflow reconfiguration—a 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–78. Springer-Verlag
[60]
The Maude System (2015) http://maude.cs.uiuc.edu. Accessed 4 Aug 2016.
[61]
Mazzara M (2006) Towards abstractions for web services composition. PhD thesis, University of Bologna Department of Computer Science
[62]
Mazzara M LTL-based verification of reconfigurable workflows Appl Math Sci 2014 8 172 8581-8600
[63]
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–177
[64]
Le Metayer D (1996) Software architecture styles as graph grammars. In: Proceedings of the 4th symposium on the foundations of software engineering, pp 15–23
[65]
Milner R (1989) Communication and concurrency. Prentice-Hall, Inc., Upper Saddle River, NJ
[66]
Milner R (1999) Communicating and mobile systems: the π-calculus. Cambridge University Press, Cambridge
[67]
Mokhov A and Khomenko V Algebra of parameterised graphs ACM Trans Embed Comput 2014 13 4s 1-22
[68]
Meyer R, Khomenko V, and Strazny T A practical approach to verification of mobile systems using net unfoldings Fundam Inform 2009 94 3–4 439-471
[69]
Mens T, Magee J, and Rumpe B Evolving software architecture descriptions of critical systems IEEE Comput 2010 43 5 42-48
[70]
Mokhov A (2009) Conditional partial order graphs. PhD thesis, Newcastle University
[71]
Montgomery J A model for updating real-time applications Real-Time Syst 2004 27 2 169-189
[72]
Milner R, Parrow J, and Walker D A calculus of mobile processes, parts I and II Inf Comput 1992 100 1 1-77
[73]
Mokhov A, Rykunov M, Sokolov D, and Yakovlev A Design of processors with reconfigurable microarchitecture J Low Power Electron Appl 2014 4 1 26-43
[74]
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–24
[75]
Medvidovic N and Taylor RN A classification and comparison framework for software architecture description languages IEEE Trans Softw Eng 2000 26 1 70-93
[76]
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–137
[77]
Mokhov A and Yakovlev A Conditional partial order graphs: model, synthesis and application IEEE Trans Comput 2010 59 11 1480-1493
[78]
Nielsen M, Plotkin GD, and Winskel G Petri nets, event structures and domains, part I Theor Comput Sci 1981 13 85-108
[79]
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–57
[80]
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–42
[81]
Pedro PSM (1999) Schedulability of mode changes in flexible real-time distributed systems. PhD thesis, University of York Department of Computer Science
[82]
Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE annual symposium on foundations of computer science, pp 46–57
[83]
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–494
[84]
Pugliese R and Tiezzi F A calculus for orchestration of web services J Appl Log 2012 10 2-31
[85]
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–185
[86]
Rensink A (2003) The GROOVE simulator: a tool for state space generation. In: Pfaltz JL, Nagl M, Böhlen B (eds) Applications of graph transformations with industrial relevance. Springer, pp 479–485
[87]
Rounds WC, Song H (2003) The Φ-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–449
[88]
Sangiorgi D (1993) Expressing mobility in process algebras: first-order and higher-order paradigms. PhD thesis, University of Edinburgh Department of Computer Science
[89]
SEN3. The Reo Project (2008). http://reo.project.cwi.nl/reo/wiki. Accessed 4 Aug 2016
[90]
Sha L, Rajkumar R, Lehoczky J, and Ramamritham K Mode change protocols for priority-driven preemptive scheduling J Real-Time Syst 1989 1 3 243-264
[91]
Stewart DB, Volpe RA, and Khosla PK Design of dynamically reconfigurable real-time software using port-based objects IEEE Trans Softw Eng 1997 23 12 759-776
[92]
Sangiorgi D and Walker D The π-calculus: a theory of mobile processes 2001 Cambridge Cambridge University Press
[93]
Taentzer G (2003) AGG: a graph transformation environment for modeling and validation of software. In: Pfaltz JL, Nagl M, Böhlen B (eds) Applications of graph transformations with industrial relevance. Springer, pp 446–453
[94]
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–109
[95]
Thomsen B (1990) Calculi for higher order communicating systems. PhD thesis, University of London Imperial College of Science, Technology and Medicine Department of Computing
[96]
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–162
[97]
Victor B, Moller F (1994) The mobility workbench—a tool for the π-calculus. In: Proceedings of the 6th international conference on computer aided verification, pp 428–440. Springer-Verlag
[98]
Wermelinger MA (1999) Specification of software architecture reconfiguration. PhD thesis, University of Lisbon Department of Informatics
[99]
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–79
[100]
Wermelinger M, Lopes A, and Fiadeiro JL A graph based architectural (re)configuration language ACM SIGSOFT Softw Eng Notes 2001 26 5 21-32
[101]
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–434
Index Terms
- An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems
Index terms have been assigned to the content through auto-classification.
Recommendations
Specification and Animation of a Bank Transfer using KIDS/VDM
The development of formal specifications may benefit from prototyping activities. The production of an executable model for a given description helps bridging the gap between this specification and the corresponding reality. The KIDS/VDM system, based on ...
Automated translation of VDM to JML-annotated Java
When a system specified using the Vienna Development Method (VDM) is realised using code-generation, no guarantees are currently made about the correctness of the generated code. In this paper, we improve code-generation of VDM models by taking contract-...
Modeling and analysis of complex computer systems-the MTCCS approach
ICECCS '96: Proceedings of the 2nd IEEE International Conference on Engineering of Complex Computer SystemsThe paper presents results from work in progress on finding a method for formal specification and verification of real time concurrent systems that incorporate a non trivial data component. We have extended Timed CCS, a timed CCS variant with a model ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© The Author(s) 2017.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 March 2017
Accepted: 07 September 2016
Received: 25 April 2016
Published in FAC Volume 29, Issue 2
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 56Total Downloads
- Downloads (Last 12 months)30
- Downloads (Last 6 weeks)6
Reflects downloads up to 04 Oct 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in