A Categorical Approach for Modeling and Verifying Dynamic Software Architecture

The dynamism in Software Architecture, also known as dynamic software architecture, is defined as the description of a system´s structural evolution as execution progresses. It brings the challenge to the system´s specification to incorporate the dynamic evolution patterns, as well as the verification of the system´s properties. Community is an Architecture Description Language built on coordination principles and a categorical framework to support the composition of specifications of components to form the system´s specification. However, an important problem of Community is the lack of support for specifying the system´s architectural changes in both the set of components and the connections between them. This paper presents an extension of Community to support the specification of the dynamism in component-based systems. The categorical approach and architectural design principles supported by the language are illustrated through the design of a fault-tolerant, dynamic client-server system, from which some of the system´s properties can be verified.