×

zbMATH — the first resource for mathematics

Interactive verification of architectural design patterns in FACTum. (English) Zbl 1425.68273
Summary: Architectural design patterns (ADPs) are architectural solutions to common architectural design problems. They are an important concept in software architectures used for the design and analysis of architectures. An ADP usually constrains the design of an architecture and, in turn, guarantees some desired properties for architectures implementing it. Sometimes, however, the constraints imposed by an ADP do not lead to the claimed guarantee. Thus, applying such patterns for the design of architectures might result in architectures which do not fulfill their intended requirements. To address this problem, we propose an approach for the verification of ADPs, based on interactive theorem proving. To this end, we introduce a model for dynamic architectures and a language for the specification of ADPs over this model. Moreover, we propose a framework for the interactive verification of such specifications based on Isabelle/HOL. In addition we describe an algorithm to map a specification to a corresponding Isabelle/HOL theory over our framework. To evaluate the approach, we implement it in Eclipse/EMF and use it for the verification of four ADPs: variants of the Singleton, the Publisher-Subscriber, the Blackboard pattern, and a pattern for Blockchain architectures. With our approach we complement traditional approaches for the verification of architectures, which are usually based on automatic verification techniques such as model checking.

MSC:
68Q65 Abstract data types; algebraic specification
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Allen, R., Douence, R., Garlan, D.: Specifying and analyzing dynamic software architectures. In: Egidio, A. (ed.) Fundamental approaches to software engineering. Lecture notes in computer science, vol. 1382, pp. 21-37. Springer, Berlin (1998)
[2] Allen, R.J.: A formal approach to software architecture. Technical report, DTIC Document (1997)
[3] Aguirre N, Maibaum T (2002) Reasoning about reconfigurable object-based systems in a temporal logic setting. In: Proceedings of IDPT
[4] Aguirre N, Maibaum T (2002) A temporal logic approach to the specification of reconfigurable component-based systems. In: Automated software engineering. IEEE, pp 271-274
[5] Arbab, F.: Reo: a channel-based coordination model for component composition. Math Struct Comput Sci 14(03), 329-366 (2004) · Zbl 1085.68552
[6] Ballarin, C.: Locales and locale expressions in isabelle/isar. Lect Notes Comput Sci 3085, 34-50 (2004) · Zbl 1100.68615
[7] Bertot, Y., Castéran, P.: Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer, Berlin (2013) · Zbl 1069.68095
[8] Bass, L., Clements, P., Kazman, R.: Software architecture in practice. Addison-Wesley, Boston (2007)
[9] Bergner K (1996) Spezifikation großer Objektgeflechte mit Komponentendiagrammen. Ph.D. thesis, Technische Universität München
[10] Bettini, L.: Implementing domain-specific languages with Xtext and Xtend. Packt Publishing Ltd, Birmingham (2016)
[11] Broy M, Facchi C, Grosu R et al (1993) The requirement and design specification language spectrum – an informal introduction. Technical report, Technische Universität München
[12] Blanchette JC, Hölzl J, Lochbihler A, Panny L, Popescu A, Traytel D (2014) Truly modular (co) datatypes for isabelle/hol. In: International conference on interactive theorem proving. Springer, pp 93-110 · Zbl 1416.68151
[13] Bergstra, J.A., Klop, J.W.: Algebra of communicating processes. CWI Monograph Ser 3, 89-138 (1986) · Zbl 0605.68013
[14] Buschmann, F., Meunier, R., Rohnert, H., Sommerlad, P., Stal, M.: Pattern-oriented software architecture: a system of patterns. Wiley, West Sussex (1996)
[15] Broy, M., Algebraic specification of reactive systems, 487-503 (1996), Berlin
[16] Broy, M.: A logical basis for component-oriented software and systems engineering. Comput J 53(10), 1758-1782 (2010)
[17] Broy M (2014) A model of dynamic systems. In: Saddek B, Yassine L, Axel L (eds) From programs to systems. The systems perspective in computing, volume 8415 of Lecture notes in computer science, pp 39-53. Springer, Berlin · Zbl 1417.68022
[18] Broy, M., Stolen, K.: Specification and development of interactive systems: focus on streams, interfaces, and refinement. Springer, Berlin (2001) · Zbl 0981.68115
[19] Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in reo by constraint automata. Sci Comput Program 61(2), 75-113 (2006) · Zbl 1105.68058
[20] Castro PF, Aguirre NM, Pombo CGL, Maibaum TSE (2010) Towards managing dynamic reconfiguration of software systems in a categorical setting. In: Lecture notes in computer science. Springer, pp 306-321
[21] Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: Nusmv: a new symbolic model checker. Int J Softw Tools Technol Trans 2(4), 410-425 (2000) · Zbl 1059.68582
[22] Canal C, Cámara J, Salaün G (2012) Structural reconfiguration of systems under behavioral adaptation. Sci Comput Program 78(1):46-64. Special Section: Formal Aspects of Component Software (FACS’09)
[23] Chandy, K.M.: Parallel program design. Springer, Berlin (1989)
[24] Dashofy EM, Van der Hoek A, Taylor RN (2001) A highly-extensible, xml-based architecture description language. In: Working IEEE/IFIP conference on software architecture, 2001. Proceedings, pp 103-112. IEEE
[25] Feiler PH, Lewis BA, Vestal S (2006) The sae architecture analysis & design language (aadl) a standard for engineering performance critical systems. In: Computer aided control system design, control applications, intelligent control. IEEE, pp 1206-1211
[26] Fiadeiro, J.L., Maibaum, T.: Categorical semantics of parallel program design. Sci Comput Program 28(2-3), 111-138 (1997) · Zbl 0877.68080
[27] Fensel D, Schnogge A (November 1997) Using kiv to specify and verify architectures of knowledge-based systems. In: Automated software engineering, pp 71-80
[28] Garlan D (2003) Formal modeling and analysis of software architecture: components, connectors, and events. In: Formal methods for software architectures, pp 1-24. Springer
[29] Gibbons, J., Hutton, G.: Proof methods for corecursive programs. Fundam Inf 66, 353-366 (2005) · Zbl 1098.68028
[30] Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design patterns: elements of reusable object-oriented software. Addison-Wesley, New York (1994) · Zbl 0887.68013
[31] Göthel T, Jähnig N, Seif S (2017) Refinement-based modelling and verification of design patterns for self-adaptive systems. In: International conference on formal engineering methods. Springer, pp 157-173
[32] Gidey HK, Marmsoler D (2018) FACTum studio. https://habtom.github.io/factum/. Accessed 19 July 2019
[33] Gidey HK, Marmsoler D, Eckhardt J (April 2017) Grounded architectures: using grounded theory for the design of software architectures. In: 2017 IEEE international conference on software architecture workshops (ICSAW), pp 141-148
[34] Garlan, D., Monroe, R.T., Wile, D.: ACME: architectural description of component-based systems. Found Component Based Syst 68, 47-68 (2000)
[35] Gorlick MM, Razouk RR (1991) Using weaves for software construction and analysis. In: Les B, David RB, Koji T (eds) Proceedings of the 13th international conference on software engineering, Austin, TX, USA, 13-17 May 1991. IEEE Computer Society, pp 23-34
[36] Gibson-Robinson T, Armstrong P, Boulgakov A, Roscoe AW (2014) Fdr3—a modern refinement checker for csp. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, pp 187-201 · Zbl 1392.68300
[37] Hölzl F, Feilkas M (2010) Autofocus 3: a scientific tool prototype for model-based development of component-based, reactive, distributed systems. In: Proceedings of the 2007 international Dagstuhl conference on model-based engineering of embedded real-time systems, MBEERTS’07, Berlin, Heidelberg. Springer, pp 317-322
[38] Hoare, C.A.R.: Communicating sequential processes. Commun ACM 21(8), 666-677 (1978) · Zbl 0383.68028
[39] Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans Softw Eng Methodol (TOSEM) 11(2), 256-290 (2002)
[40] Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. EATCS Bull 62, 62-222 (1997) · Zbl 0880.68070
[41] Kim JS, Garlan D (2006) Analyzing architectural styles with alloy. In: Proceedings of the ISSTA 2006 workshop on Role of software architecture for testing and analysis. ACM, pp 70-80
[42] Klein MH, Kazman R, Bass L, Carriere J, Barbacci M, Lipson H (1999) Attribute-based architecture styles. In: Software architecture. Springer, pp 225-243
[43] Krause C, Maraikar Z, Lazovik A, Arbab F (2011) Modeling dynamic reconfigurations in reo using high-level replacement systems. Sci Comput Program 76(1):23-36. Selected papers from the 6th international workshop on the foundations of coordination languages and software architectures · Zbl 1211.68052
[44] Kiayias A, Russell A, David B, Oliynykov R (2017) Ouroboros: a provably secure proof-of-stake blockchain protocol. In: Annual international cryptology conference. Springer, pp 357-388 · Zbl 1407.94128
[45] Luckham, D.C., Kenney, J.J., Augustin, L.M., Vera, J., Bryan, D., Mann, W.: Specification and analysis of system architecture using rapide. IEEE Trans Softw Eng 21(4), 336-354 (1995)
[46] Laroussinie F, Meyer A, Petonnet E (2010) Counting LTL. In: 2010 17th international symposium on temporal representation and reasoning. IEEE · Zbl 1284.03149
[47] Lochbihler A (2010) Coinduction. The archive of formal proofs. http://afp.sourceforge.net/entries/Coinductive.shtml.Accessed 19 July 2019
[48] Li, Y., Sun, M.: Modeling and analysis of component connectors in coq. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) Formal aspects of component software-10th international symposium, FACS 2013, Nanchang, China, 27-29 Oct 2013, Revised selected papers. Lecture notes in computer science, vol. 8348, pp. 273-290. Springer (2013)
[49] Marmsoler D (2010) Applying the scientific method in the definition and analysis of a new architectural style. Master’s thesis, Free University of Bolzano-Bozen
[50] Marmsoler D (2017) Dynamic architectures. Archive of formal proofs. http://isa-afp.org/entries/DynamicArchitectures.html. Formal proof development. Accessed 19 July 2019 · Zbl 1444.68120
[51] Marmsoler, D.: Towards a calculus for dynamic architectures. In: Van Hung, D., Kapur, D. (eds.) Theoretical aspects of computing-ICTAC 2017-14th international colloquium, Hanoi, Vietnam, 23-27 Oct 2017, Proceedings. Lecture notes in computer science, vol. 10580, pp. 79-99. Springer (2017)
[52] Marmsoler D (2018) A framework for interactive verification of architectural design patterns in isabelle/hol. In: The 20th international conference on formal engineering methods, ICFEM 2018, Proceedings
[53] Marmsoler D (2018) A theory of architectural design patterns. Archive of formal proofs. http://isa-afp.org/entries/Architectural_Design_Patterns.html. Formal proof development
[54] Mak JKH, Choy CST, Lun DPK (2004) Precise modeling of design patterns in uml. In: Software engineering. IEEE, pp 252-261
[55] Marmsoler D, Degenhardt S (2017) Verifying patterns of dynamic architectures using model checking. In: Proceedings international workshop on formal engineering approaches to software components and architectures, FESCA@ETAPS 2017, Uppsala, Sweden, 22nd April 2017, pp 16-30
[56] Marmsoler, D., Gleirscher, M.: On activation, connection, and behavior in dynamic architectures. Sci Ann Comput Sci 26(2), 187-248 (2016) · Zbl 1424.68003
[57] Marmsoler D, Gleirscher M (2016) Specifying properties of dynamic architectures using configuration traces. In: International colloquium on theoretical aspects of computing. Springer, pp 235-254 · Zbl 06667710
[58] Marmsoler D, Gidey HK (2018) FACTum Studio: a tool for the axiomatic specification and verification of architectural design patterns. In: Formal aspects of component software—FACS 2018—15th international conference, Proceedings
[59] Milner, R.: Communicating and mobile systems: the \[\pi\] π-calculus. Cambridge University Press, Cambridge (1999) · Zbl 0942.68002
[60] Magee J, Kramer J (1996) Dynamic structure in software architectures. In: Garlan D (ed) SIGSOFT’96, Proceedings of the fourth ACM SIGSOFT symposium on foundations of software engineering, San Francisco, California, USA, 16-18 Oct 1996. ACM, pp 3-14
[61] Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, New York (1992)
[62] Nakamoto S (2008) Bitcoin: a peer-to-peer electronic cash system
[63] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic, vol. 2283. Springer, Berlin (2002) · Zbl 0994.68131
[64] Oquendo, \[F.: \pi\] π-adl: an architecture description language based on the higher-order typed \[\pi\] π-calculus for specifying dynamic and mobile software architectures. ACM SIGSOFT Softw Eng Notes 29(3), 1-14 (2004)
[65] Rausch A (2001) Componentware. Dissertation, Technische Universität München, München
[66] Reif W (1995) The kiv-approach to software verification. In: KORSO: methods, languages, and tools for the construction of correct software, pp 339-368
[67] Rumbaugh, J., Jacobson, I., Booch, G.: The unified modeling language reference manual. Pearson Higher Education, New York (2004)
[68] Sanchez, A.; Barbosa, LS; Riesco, D.; Arbab, F. (ed.); Ölveczky, PC (ed.), Bigraphical modelling of architectural patterns, 313-330 (2012), Berlin
[69] Shaw, M., Garlan, D.: Software architecture: perspectives on an emerging discipline, vol. 1. Prentice Hall, Englewood Cliffs (1996) · Zbl 0948.68506
[70] Soundarajan N, Hallstrom JO (2004) Responsibilities and rewards: specifying design patterns. In: Software engineering. IEEE, pp 666-675
[71] Sanchez, A., Madeira, A., Barbosa, L.S.: On the verification of architectural reconfigurations. Comput Lang Syst Struct 44, 218-237 (2015) · Zbl 1387.68071
[72] Spichkova M (2007) Specification and seamless verification of embedded real-time systems: FOCUS on Isabelle. Ph.D. thesis, Technical University Munich, Germany
[73] Taylor, R.N., Medvidovic, N., Dashofy, E.M.: Software architecture: foundations, theory, and practice. Wiley, Hoboken (2009)
[74] TypeFox and Obeo (2017) Xtext/sirius—integration the main use-cases. https://goo.gl/8bcWJc
[75] van Ommering, R.C., van der Linden, F., Kramer, J., Magee, J.: The koala component model for consumer electronics software. IEEE Comput 33(3), 78-85 (2000)
[76] Wenzel M et al (2004) The isabelle/isar reference manual
[77] Wenzel, M.: Isabelle/isar–a generic framework for human-readable proof documents. From Insight to Proof-Festschrift in Honour of Andrzej Trybulec 10(23), 277-298 (2007)
[78] Wermelinger M, Fiadeiro JL (2002) A graph transformation approach to software architecture reconfiguration. Sci Comput Program 44(2):133 - 155. Special Issue on Applications of Graph Transformations (GRATRA 2000) · Zbl 1014.68033
[79] Wirsing, M.; Leeuwen, J. (ed.), Algebraic specification, No. B, 675-788 (1990), Cambridge · Zbl 0900.68309
[80] Wermelinger M, Lopes A, Fiadeiro JL (2001) A graph based architectural (re)configuration language. In: Software engineering notes, vol 26. ACM, pp 21-32
[81] Wong S, Sun J, Warren I, Sun J (2008) A scalable approach to multi-style architectural modeling and verification. In: Engineering of complex computer systems. IEEE, pp 25-34
[82] Zdun U, Avgeriou P (2005) Modeling architectural patterns using architectural primitives. In: Johnson RE, Gabriel RP (eds) Proceedings of the 20th annual ACM SIGPLAN conference on object-oriented programming, systems, languages, and applications, OOPSLA 2005, 16-20 Oct 2005, San Diego, CA, USA, pp 133-146. ACM
[83] Zhang J, Liu Y, Sun J, Dong JS, Sun J (2012) Model checking software architecture design. In: High-assurance systems engineering. IEEE, pp 193-200
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.