Specifying properties of dynamic architectures using configuration traces

Abstract

The architecture of a system describes the system’s overall organization into components and connections between those components. With the emergence of mobile computing,dynamic architectures became increasingly important. In such architectures,components may appear or disappear,and connections may change over time. Despite the growing importance of dynamic architectures,the specification of properties for those architectures remains a challenge. To address this problem,we introduce the notion of configuration traces to model properties of dynamic architectures. Then,we investigate these properties to identify different types thereof. We show completeness and consistency of these types,i.e.,we show that (almost) every property can be separated into these types and that a property of one type does not impact properties of other types. Configuration traces can be used to specify general properties of dynamic architectures and the separation into different types provides a systematic way for their specification. To evaluate our approach we apply it to the specification and verification of the Blackboard pattern in Isabelle/HOL.