Study On Formal Description Of Software Architecture

Software architecture plays a critical role in almost all aspects of the software development lifecycle. Graphical languages are widely used in software architectural modeling. They are intuitive and more formal than natural languages. However, the lack of precise semantics makes it difficult to analyze the models they describe. In this aspect, formal methods can be used complementarily. It is now a common concern among industrial and academic communities on how to combine the merits of these two kinds of methods and thereby improve the software reliability.We propose a dual framework, XYZ/ADL, for software architecture description. It supports the basic concepts of software architecture commonly used in software engineering. The front end of XYZ/ADL is a collection of graphical modeling languages, including the usual "box-and-line" diagrams as architectural structure expression, and the UML activity diagrams and Statecharts as behavioral expression. Its back end is a linear temporal logic language, XYZ/E, which can represent both dynamic semantics and static semantics of systems, as its unified formal semantic backbone. The graphical languages at front end can facilitate the communication among software engineers and their use of this framework. The formal language at the back end is the basis of formal analysis and verification.The main contributions of this thesis are:· This thesis proposes a dual framework for software architecture description, combining "box-and-line" architectural diagrams, UML activity diagrams, and Statecharts as front end graphical modeling languages, and XYZ/E as its unified formal semantic backbone.· This thesis provides semantics for elements of software architecture usingXYZ/E, and extends XYZ/E to explicitly support the basic concepts of software architecture. These extensions are then defined rigorously using XYZ/E. The XYZ/ADL provides features that are acknowledged widely in software engineering community.· This thesis defines temporal logic semantics for UML activity diagrams and Statecharts using XYZ/E. They can be used with rigorous semantics under our description framework. Furthermore, because these two graphical languages can be used in other stage of software development, our formal semantic definition can be the basis for the analysis and verification of models they specify in those stages.