On the Specification of Constraints for Dynamic Architectures

TL;DR

This paper presents a formal approach using configuration traces, assertions, and diagrams to specify and verify constraints and patterns in dynamic architectures, enhancing focus on architecture constraints over concrete instances.

Contribution

It introduces a formal language and graphical notation for specifying and verifying constraints in dynamic architectures, focusing on architecture patterns rather than concrete configurations.

Findings

Effective specification of architecture patterns using the proposed formalism

Verification of the Blackboard pattern demonstrates approach's applicability

Supports formal analysis of dynamic architecture constraints

Abstract

In dynamic architectures, component activation and connections between components may vary over time. With the emergence of mobile computing such architectures became increasingly important and several techniques emerged to support in their specification. These techniques usually allow for the specification of concrete architecture instances. Sometimes, however, it is desired to focus on the specification of constraints, rather than concrete architectures. Especially specifications of architecture patterns usually focus on a few, important constraints, leaving out the details of the concrete architecture implementing the pattern. With this article we introduce an approach to specify such constraints for dynamic architectures. To this end, we introduce the notion of configuration traces as an abstract model for dynamic architectures. Then, we introduce the notion of configuration trace assertions as a formal language based on linear temporal logic to specify constraints for such architectures. In addition, we also introduce the notion of configuration diagrams to specify interfaces and certain common activation and connection constraints in one single, graphical notation. The approach is well-suited to specify patterns for dynamic architectures and verify them by means of formal analyses. This is demonstrated by applying the approach to specify and verify the Blackboard pattern for dynamic architectures.