{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:06:19Z","timestamp":1762459579043,"version":"3.37.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319893624"},{"type":"electronic","value":"9783319893631"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89363-1_9","type":"book-chapter","created":{"date-parts":[[2018,4,3]],"date-time":"2018-04-03T09:04:43Z","timestamp":1522746283000},"page":"149-168","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Hierarchical Specification and Verification of Architectural Design Patterns"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2859-7673","authenticated-orcid":false,"given":"Diego","family":"Marmsoler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,4]]},"reference":[{"key":"9_CR1","volume-title":"Software Architecture: Foundations, Theory, and Practice","author":"RN Taylor","year":"2009","unstructured":"Taylor, R.N., Medvidovic, N., Dashofy, E.M.: Software Architecture: Foundations, Theory, and Practice. Wiley Publishing, Chichester (2009)"},{"key":"9_CR2","volume-title":"Pattern-Oriented Software Architecture: A System of Patterns","author":"F Buschmann","year":"1996","unstructured":"Buschmann, F., Meunier, R., Rohnert, H., Sommerlad, P., Stal, M.: Pattern-Oriented Software Architecture: A System of Patterns. Wiley, West Sussex (1996)"},{"key":"9_CR3","volume-title":"Software Architecture: Perspectives on an Emerging Discipline","author":"M Shaw","year":"1996","unstructured":"Shaw, M., Garlan, D.: Software Architecture: Perspectives on an Emerging Discipline, vol. 1. Prentice Hall, Englewood Cliffs (1996)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/11542384","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol. 3600. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11542384"},{"issue":"2","key":"9_CR5","first-page":"187","volume":"26","author":"D Marmsoler","year":"2016","unstructured":"Marmsoler, D., Gleirscher, M.: On activation, connection, and behavior in dynamic architectures. Sci. Ann. Comput. Sci. 26(2), 187\u2013248 (2016)","journal-title":"Sci. Ann. Comput. Sci."},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-46750-4_14","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"D Marmsoler","year":"2016","unstructured":"Marmsoler, D., Gleirscher, M.: Specifying properties of dynamic architectures using configuration traces. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 235\u2013254. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-46750-4_14"},{"key":"9_CR7","unstructured":"Marmsoler, D.: Dynamic architectures. Archive of Formal Proofs, pp. 1\u201365. Formal proof development, July 2017"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67729-3_6","volume-title":"heoretical Aspects of Computing \u2013 ICTAC 2017","author":"D Marmsoler","year":"2017","unstructured":"Marmsoler, D.: Towards a calculus for dynamic architectures. In: Hung, D., Kapur, D. (eds.) ICTAC 2017. LNCS, vol. 10580. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-67729-3_6"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"MJ Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979). \nhttps:\/\/doi.org\/10.1007\/3-540-09724-4"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-48256-3_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S Berghofer","year":"1999","unstructured":"Berghofer, S., Wenzel, M.: Inductive datatypes in HOL \u2014 lessons learned in formal-logic engineering. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 19\u201336. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-48256-3_3"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 307\u2013322. Springer, Heidelberg (1997). \nhttps:\/\/doi.org\/10.1007\/BFb0028402"},{"key":"9_CR13","unstructured":"Wenzel, M.: Isabelle\/Isar - a generic framework for human-readable proof documents. In: From Insight to Proof - Festschrift in Honour of Andrzej Trybulec vol. 10, no. 23, pp. 277\u2013298 (2007)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-24849-1_3","volume-title":"Types for Proofs and Programs","author":"C Ballarin","year":"2004","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 34\u201350. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24849-1_3"},{"issue":"10","key":"9_CR15","doi-asserted-by":"crossref","first-page":"1758","DOI":"10.1093\/comjnl\/bxq005","volume":"53","author":"M Broy","year":"2010","unstructured":"Broy, M.: A logical basis for component-oriented software and systems engineering. Comput. J. 53(10), 1758\u20131782 (2010)","journal-title":"Comput. J."},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-54848-2_3","volume-title":"From Programs to Systems. The Systems perspective in Computing","author":"M Broy","year":"2014","unstructured":"Broy, M.: A model of dynamic systems. In: Bensalem, S., Lakhneck, Y., Legay, A. (eds.) ETAPS 2014. LNCS, vol. 8415, pp. 39\u201353. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54848-2_3"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Marmsoler, D.: On the semantics of temporal specifications of component-behavior for dynamic architectures. In: Eleventh International Symposium on Theoretical Aspects of Software Engineering. Springer (2017)","DOI":"10.1109\/TASE.2017.8285638"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/BFb0014335","volume-title":"Algebraic Methodology and Software Technology","author":"M Broy","year":"1996","unstructured":"Broy, M.: Algebraic specification of reactive systems. In: Wirsing, M., Nivat, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 487\u2013503. Springer, Heidelberg (1996). \nhttps:\/\/doi.org\/10.1007\/BFb0014335"},{"key":"9_CR19","first-page":"675","volume-title":"Handbook of Theoretical Computer Science","author":"M Wirsing","year":"1990","unstructured":"Wirsing, M.: Algebraic specification. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 675\u2013788. MIT Press, Cambridge (1990)"},{"key":"9_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992). \nhttps:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"key":"9_CR21","unstructured":"Wenzel, M., et al.: The Isabelle\/Isar reference manual (2004)"},{"key":"9_CR22","unstructured":"Marmsoler, D.: Isabelle\/HOL theories for the singleton, publisher subscriber, and blackboard pattern. \nhttp:\/\/www.marmsoler.com\/docs\/FASE18"},{"key":"9_CR23","unstructured":"Allen, R.J.: A formal approach to software architecture. Technical report, DTIC Document (1997)"},{"issue":"2","key":"9_CR24","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/s00165-015-0349-8","volume":"28","author":"P Attie","year":"2016","unstructured":"Attie, P., Baranov, E., Bliudze, S., Jaber, M., Sifakis, J.: A general framework for architecture composability. Form. Asp. Comput. 28(2), 207\u2013231 (2016)","journal-title":"Form. Asp. Comput."},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Mavridou, A., Baranov, E., Bliudze, S., Sifakis, J.: Architecture diagrams: a graphical language for architecture style specification. In: Bartoletti, M., Henrio, L., Knight, S., Vieira, H.T. (eds.) Proceedings of the 9th Interaction and Concurrency Experience. ICE 2016, Heraklion, 8\u20139 June 2016. EPTCS, vol. 223, pp. 83\u201397 (2016)","DOI":"10.4204\/EPTCS.223.6"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-319-28934-2_14","volume-title":"Formal Aspects of Component Software","author":"A Mavridou","year":"2016","unstructured":"Mavridou, A., Baranov, E., Bliudze, S., Sifakis, J.: Configuration logics: modelling architecture styles. In: Braga, C., \u00d6lveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 256\u2013274. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-28934-2_14"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Kim, J.S., Garlan, D.: Analyzing architectural styles with alloy. In: Proceedings of the ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis, pp. 70\u201380. ACM (2006)","DOI":"10.1145\/1147249.1147259"},{"issue":"2","key":"9_CR28","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. (TOSEM) 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-39800-4_1","volume-title":"Formal Methods for Software Architectures","author":"D Garlan","year":"2003","unstructured":"Garlan, D.: Formal modeling and analysis of software architecture: components, connectors, and events. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol. 2804, pp. 1\u201324. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-39800-4_1"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Wong, S., Sun, J., Warren, I., Sun, J.: A scalable approach to multi-style architectural modeling and verification. In: Engineering of Complex Computer Systems, pp. 25\u201334. IEEE (2008)","DOI":"10.1109\/ICECCS.2008.16"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Zhang, J., Liu, Y., Sun, J., Dong, J.S., Sun, J.: Model checking software architecture design. In: High-Assurance Systems Engineering, pp. 193\u2013200. IEEE (2012)","DOI":"10.1109\/HASE.2012.12"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Marmsoler, D., Degenhardt, S.: Verifying patterns of dynamic architectures using model checking. In: Proceedings of the International Workshop on Formal Engineering approaches to Software Components and Architectures, FESCA@ETAPS 2017, Uppsala, Sweden, 22 April 2017, pp. 16\u201330 (2017)","DOI":"10.4204\/EPTCS.245.2"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-34005-5_4","volume-title":"Rewriting Logic and Its Applications","author":"M Wirsing","year":"2012","unstructured":"Wirsing, M., Eckhardt, J., M\u00fchlbauer, T., Meseguer, J.: Design and analysis of cloud-based architectures with KLAIM and Maude. In: Dur\u00e1n, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 54\u201382. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-34005-5_4"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Fensel, D., Schnogge, A.: Using KIV to specify and verify architectures of knowledge-based systems. In: Automated Software Engineering, pp. 71\u201380, November 1997","DOI":"10.1109\/ASE.1997.632826"},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-07602-7_17","volume-title":"Formal Aspects of Component Software","author":"Y Li","year":"2014","unstructured":"Li, Y., Sun, M.: Modeling and analysis of component connectors in Coq. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 273\u2013290. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-07602-7_17"},{"issue":"03","key":"9_CR36","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1017\/S0960129504004153","volume":"14","author":"F Arbab","year":"2004","unstructured":"Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(03), 329\u2013366 (2004)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Marmsoler, D.: Towards a theory of architectural styles. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering\u00a0- FSE 2014, pp. 823\u2013825. ACM Press (2014)","DOI":"10.1145\/2635868.2661683"},{"key":"9_CR38","volume-title":"EMF: Eclipse Modeling Framework","author":"D Steinberg","year":"2008","unstructured":"Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework. Pearson Education, London (2008)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89363-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,3]],"date-time":"2018-04-03T09:11:07Z","timestamp":1522746667000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89363-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319893624","9783319893631"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89363-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}