This book gathers together the papers that were presented at the Third International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SEM03), in Italy. The main focus of this conference was on the applications of formal methods in software architectures, which includes topics in the architectural description languages (ADLs), tools, architectural modeling, architectural evolutions, and architectural analysis and testing.

The first paper in the book, presented by David Garlan, sets the tone for the entire conference. The paper discusses the problem of correctly and formally specifying architectural style, using Acme style. The paper by Axel van Lamsweerde discusses the problem of filling the gap between system goals (or requirements) and software architecture, using a goal-oriented method known as the KAOS framework. The paper by Kramer et al. discusses the authors’ tool-supported approach to the design and analysis of large and complex software systems, at a high level of abstraction, using Darwin’s ADL.

The short paper by Wolf et al. highlights the importance of architectural analysis, namely dependence analysis. The paper by Kaveh and Emmerich concerns the validation of distributed software systems based on object or component middleware. More specifically, the authors propose a method to specify safety and liveness properties in the unified modeling language (UML), and then map these representations into process algebra safety and liveness properties. Model checking would then be used to verify the design.

The paper by Inverardi and Tivoli addresses issues in the correct assembly of off-the-shelf components (COTS). More specifically, the authors discuss management of the dynamic interactions of the COTS, and provide a solution for the detection/recovery of COTS integration anomalies using the specification of the system. The next paper, also by Inverardi et al., discusses a code testing method using software architecture.

The paper by Andrade and Fiaderio discusses the importance of software architecture in evolvable and adaptable systems. More specifically, the authors identify existing problems, and propose a remedy based on computation, coordination, and configuration. The paper by Murphy et al. discusses a solution to control the complexity of applications for mobile systems, based on formal middleware modeling.

The remaining papers address the evaluation of nonfunctional requirements, namely performance and dependability at the architectural level. The paper by Balsamo et al. discusses a methodology based on Emilla and stochastic process algebra, in order to evaluate and predict the performance of different software architectures for given requirements. The last paper, by Issarny and Zarras, discusses software architecture and dependability. To this end, the paper presents a method using a dependability analysis technique, and its representation in UML.

This book represents a body of work and knowledge written by leading researchers who helped envision the concept of software architecture, and its wide recognition. The book will be a wonderful reference for students, as well as for practitioners who are interested in architectural specifications and analysis.