Specifying software architectures using a formal-based approach

Architecture description languages (ADLs) describe the abstracted structure of a system. In this paper we describe a new ADL based on extension of the existing CARE language used informally specifying and implementing reusable software components. The main elements of this ADL are components and connectors, with functional and nonfunctional behaviours and interfaces defined. The ADL includes a configuration part, describing the connection between components and connectors, defined using a CSP-like notation. The ADL is amenable to the use of theorem proving techniques for establishing correctness of the architecture. The recursive architecture is also specified as apart of the communication. The design for the CARE ADL is incorporated with the plan to leverage existing tools for matching and adapting CARE components, to develop support for the detection and correction of architecture mismatches (i. e. where components do not interoperate correctly).