{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T20:07:18Z","timestamp":1775246838337,"version":"3.50.1"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030024499","type":"print"},{"value":"9783030024505","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-02450-5_15","type":"book-chapter","created":{"date-parts":[[2018,10,10]],"date-time":"2018-10-10T08:54:57Z","timestamp":1539161697000},"page":"251-269","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Framework for Interactive Verification of Architectural Design Patterns in Isabelle\/HOL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2859-7673","authenticated-orcid":false,"given":"Diego","family":"Marmsoler","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,10,11]]},"reference":[{"key":"15_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, Hoboken (2009)"},{"key":"15_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":"15_CR3","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-319-89363-1_9","volume-title":"Fundamental Approaches to Software Engineering","author":"Diego Marmsoler","year":"2018","unstructured":"Marmsoler, D.: Hierarchical specification and verification of architecture design patterns. In: Proceedings of Fundamental Approaches to Software Engineering, FASE 2018, Thessaloniki, Greece, 14\u201320 April 2018 (2018)"},{"key":"15_CR4","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). https:\/\/doi.org\/10.1007\/978-3-319-46750-4_14"},{"issue":"2","key":"15_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":"15_CR6","doi-asserted-by":"publisher","unstructured":"Marmsoler, D.: On the semantics of temporal specifications of component-behavior for dynamic architectures. In: 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 1\u20136. IEEE (2017). https:\/\/doi.org\/10.1109\/tase.2017.8285638","DOI":"10.1109\/tase.2017.8285638"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-67729-3_6","volume-title":"Theoretical Aspects of Computing","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, pp. 79\u201399. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67729-3_6"},{"key":"15_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"15_CR9","unstructured":"Marmsoler, D.: Dynamic architectures. Archive of Formal Proofs, July 2017. http:\/\/isa-afp.org\/entries\/DynamicArchitectures.html"},{"key":"15_CR10","unstructured":"Marmsoler, D.: A theory of architectural design patterns. Archive of Formal Proofs, March 2018. http:\/\/isa-afp.org\/entries\/Architectural_Design_Patterns.html"},{"key":"15_CR11","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). https:\/\/doi.org\/10.1007\/978-3-540-24849-1_3"},{"issue":"10","key":"15_CR12","doi-asserted-by":"publisher","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":"15_CR13","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":"15_CR14","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). https:\/\/doi.org\/10.1007\/BFb0014335"},{"key":"15_CR15","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, vol. B, pp. 675\u2013788. MIT Press, Cambridge (1990)"},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"16","DOI":"10.4204\/EPTCS.245.2","volume":"245","author":"Diego Marmsoler","year":"2017","unstructured":"Marmsoler, D., Degenhardt, S.: Verifying patterns of dynamic architectures using model checking. In: Formal Engineering Approaches to Software Components and Architectures, FESCA@ETAPS 2017, Uppsala, Sweden, 22 April 2017, pp. 16\u201330 (2017)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"15_CR17","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). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"MJ Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979). https:\/\/doi.org\/10.1007\/3-540-09724-4"},{"key":"15_CR19","unstructured":"Milner, R., Tofte, M., Harper, R.: The Definition of Standard ML. MIT Press, Cambridge (1990). Literaturverz. S. [87]\u201389"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-08970-6_7","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93\u2013110. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_7"},{"issue":"23","key":"15_CR21","first-page":"277","volume":"10","author":"M Wenzel","year":"2007","unstructured":"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\u2013298 (2007)","journal-title":"From Insight to Proof - Festschrift in Honour of Andrzej Trybulec"},{"key":"15_CR22","unstructured":"Lochbihler, A.: Coinduction. The Archive of Formal Proofs. http:\/\/afp.sourceforge.net\/entries\/Coinductive.shtml (2010)"},{"key":"15_CR23","unstructured":"Marmsoler, D.: A framework for interactive verification of architectural design patterns in Isabelle\/HOL. Electronic Supplementary Material. http:\/\/www.marmsoler.com\/docs\/ICFEM18\/"},{"key":"15_CR24","unstructured":"Bergner, K.: Spezifikation gro\u00dfer Objektgeflechte mit Komponentendiagrammen. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (1996)"},{"key":"15_CR25","unstructured":"Broy, M., Facchi, C., Grosu, R., et al.: The requirement and design specification language spectrum - an informal introduction. Technical report, Technische Universit\u00e4t M\u00fcnchen (1993)"},{"key":"15_CR26","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":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BFb0015471","volume-title":"KORSO: Methods, Languages, and Tools for the Construction of Correct Software","author":"W Reif","year":"1995","unstructured":"Reif, W.: The KIV-approach to software verification. In: Broy, M., J\u00e4hnichen, S. (eds.) KORSO: Methods, Languages, and Tools for the Construction of Correct Software. LNCS, vol. 1009, pp. 339\u2013368. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0015471"},{"key":"15_CR28","unstructured":"Spichkova, M.: Specification and seamless verification of embedded real-time systems: FOCUS on Isabelle. Ph.D. thesis, Technical University Munich, Germany (2007)"},{"key":"15_CR29","volume-title":"Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement","author":"M Broy","year":"2012","unstructured":"Broy, M., Stolen, K.: Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer, New York (2012)"},{"key":"15_CR30","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). https:\/\/doi.org\/10.1007\/978-3-319-07602-7_17"},{"key":"15_CR31","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2013","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013)"},{"issue":"03","key":"15_CR32","doi-asserted-by":"publisher","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."},{"issue":"3","key":"15_CR33","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"15_CR34","unstructured":"Merz, S.: Mechanizing TLA in Isabelle. In: Workshop on Verification in New Orientations, pp. 54\u201374. Citeseer (1995)"},{"key":"15_CR35","unstructured":"Grov, G., Merz, S.: A definitional encoding of TLA* in Isabelle\/HOL. Archive of Formal Proofs, November 2011. http:\/\/isa-afp.org\/entries\/TLA.html"},{"key":"15_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1226","DOI":"10.1007\/3-540-48118-4_15","volume-title":"FM 1999 \u2014 Formal Methods","author":"S Merz","year":"1999","unstructured":"Merz, S.: A more complete TLA. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1226\u20131244. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48118-4_15"},{"issue":"3","key":"15_CR37","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1109\/32.910858","volume":"27","author":"R Mattolini","year":"2001","unstructured":"Mattolini, R., Nesi, P.: An interval logic for real-time system specification. IEEE Trans. Softw. Eng. 27(3), 208\u2013227 (2001)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"15_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-642-03359-9_29","volume-title":"Theorem Proving in Higher Order Logics","author":"A Schimpf","year":"2009","unstructured":"Schimpf, A., Merz, S., Smaus, J.-G.: Construction of B\u00fcchi Automata for LTL model checking verified in Isabelle\/HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 424\u2013439. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_29"},{"key":"15_CR39","unstructured":"Sickert, S.: Linear temporal logic. Archive of Formal Proofs, March 2016. http:\/\/isa-afp.org\/entries\/LTL.html"},{"key":"15_CR40","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 - FSE 2014, pp. 823\u2013825. ACM Press (2014)","DOI":"10.1145\/2635868.2661683"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02450-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T19:19:32Z","timestamp":1775243972000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02450-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030024499","9783030024505"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02450-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Gold Coast, QLD","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Australia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 November 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 November 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.formal-analysis.com\/icfem\/2018\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"66","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"22","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"14","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}