Computing Publications

Publications Home » Software architecture modeling an...

Software architecture modeling and analysis: a rigorous approach

Jeff Kramer, Jeff Magee, Sebastian Uchitel

Book Chapter
Formal methods for software architectures. Third International School on Formal Methods for the Design of Computer, Communication and Software Systems: Software Architectures, SFM 2003, Bertinoro, Italy, September 22-27, 2003
Formal Methods for Software Architectures (SFM-03:SA Lectures)
Lecture Notes in Computer Science
Volume 2804
September, 2003
ISBN 3-540-20083-5
DOI 10.1007/b13225

In this overview paper, we outline a tool supported approach to the design and analysis of complex systems at the architectural level. The foundations of this approach are the use of the architectural description language Darwin to capture structural information about components and their interconnection and the use of a process algebra FSP to describe the behaviour of individual components. These descriptions are combined to construct a system behavioural model that can be animated to validate requirements and model checked against properties specified in Linear Temporal Logic. Recently, this foundation has been extended with work on the synthesis of behavioural models from scenarios captured as message sequence charts (MSC). Models described in this way can be used as an initial basis for validating requirements and as a specification that must be satisfied by more detailed models. The approach we outline is supported by the Labelled Transition system Analyser (LTSA) tool, which has been extended to deal with MSCs.

BibTEX file for the publication built & maintained by Ashok Argent-Katwala.