Dynamic Software Architectures: Formally Modelling Structure and Behaviour with Pi-ADL

A key aspect of the design of any software system is its architecture. From the perspective of dependability, an effective architecture aims to build fault-free systems, i.e. ensuring fault avoidance. At the architecture level, fault avoidance is achieved by formally describing the structure and behaviour of software systems enabling to check their correctness. Therefore, a software architecture description should provide a formal specification of the architecture in terms of components and connectors and how they behave and are composed together. Further, a dynamic software architecture must provide a specification of how the architecture of the software system can change at runtime. Enabling specification of dynamic architectures is a large challenge for an architecture description language (ADL). This paper presents how Pi-ADL, a novel ADL that has been designed in the ArchWare European Project, can be used for specifying dynamic architectures through a case study.