Software architecture modelling and analysis in process algebra

Publication Type:
Issue Date:
Full metadata record
Files in This Item:
Filename Description SizeFormat
01front.pdf211.31 kBAdobe PDF
02whole.pdf1.09 MBAdobe PDF
Description of the principal design of software-intense systems is fundamental in the diversified areas of software architecture. In the past two decades, a variety of Architecture Description Languages (ADLs) emerged and competed to be a suitable modelling medium for software architecture. The high-level syntax of these languages expresses the coarse-grained specifications and properties of interest for the systems, and their formal semantics enables a rigorous analysis of these properties. Notations from the dialect of Process Algebra (PA) are frequently employed by ADLs. The variety of ADLs and the popularity of PA in architectural description motivate the research of PA as formal notations of architectural description, independent of the high-level syntax of ADLs. One benefit of this study is to shed light on some verification techniques for the system properties that ADLs aim to deal with. This thesis investigates two basic architectural models, which are the connector- based and peer-to-peer architectures, respectively. This thesis presents a PA-based ADL-like language and a PA-based semantic approach to describe and analyse the first architectural model, and employs session types for π-calculus to deal with the second model. The main contributions are as follows. First, this thesis conducts an in-depth study on the use of PA as formal notations for modelling these architectures, and presents various analytic techniques to facilitate the verification of the system properties of interest. Second, this thesis introduces the session type theory into the field of software architecture research and improves the state of the art of the theory by structuring the session description in the communication and integration levels. Last, to enhance the adequacy of PA as ad hoc architectural modelling notations, this thesis presents an algorithm to merge a modal extension of PA and the constraint-style specifications.
Please use this identifier to cite or link to this item: