Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: A Theory of Architectural Desig...


view this post on Zulip Email Gateway (Aug 22 2022 at 16:53):

From: Tobias Nipkow <nipkow@in.tum.de>
A Theory of Architectural Design Patterns
Diego Marmsoler

The following document formalizes and verifies several architectural design
patterns. Each pattern specification is formalized in terms of a locale where
the locale assumptions correspond to the assumptions which a pattern poses on an
architecture. Thus, pattern specifications may build on top of each other by
interpreting the corresponding locale. A pattern is verified using the framework
provided by the AFP entry Dynamic Architectures. Currently, the document
consists of formalizations of 4 different patterns: the singleton, the publisher
subscriber, the blackboard pattern, and the blockchain pattern. Thereby, the
publisher component of the publisher subscriber pattern is modeled as an
instance of the singleton pattern and the blackboard pattern is modeled as an
instance of the publisher subscriber pattern. In general, this entry provides
the first steps towards an overall theory of architectural design patterns.

https://www.isa-afp.org/entries/Architectural_Design_Patterns.html

Enjoy!
smime.p7s


Last updated: Nov 21 2024 at 12:39 UTC