A Theory of Architectural Design Patterns

Title:	A Theory of Architectural Design Patterns
Author:	Diego Marmsoler
Submission date:	2018-03-01
Abstract:	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.
Change history:	[2018-05-25]: changing the major assumption for blockchain architectures from alternative minings to relative mining frequencies (revision 5043c5c71685) [2019-04-08]: adapting the terminology: honest instead of trusted, dishonest instead of untrusted (revision 7af3431a22ae)
BibTeX:	@article{Architectural_Design_Patterns-AFP, author = {Diego Marmsoler}, title = {A Theory of Architectural Design Patterns}, journal = {Archive of Formal Proofs}, month = mar, year = 2018, note = {\url{http://isa-afp.org/entries/Architectural_Design_Patterns.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	DynamicArchitectures
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry