The Dual Software Architecture Description Framework XYZ/ADL

Software architecture plays a critical role in the process of software development. Graphical languages are widely used in software architectural modeling. They have advantages of being intuitive and semi-formal. However, the lack of precise semantics makes the models difficult to analyze. In this aspect, formal methods can be used complementarily. And it is not practical to model architectures using only the formal languages in engineering development. 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. In this paper, a dual software architecture description framework, XYZ/ADL, is proposed. It supports the basic concepts of software architecture used commonly in software engineering. The front end of XYZ/ADL is a collection of graphical languages, including the usual “box-and-line” diagrams as structure expression, and the UML activity diagrams and statecharts as behavioral expression. The back end of XYZ/ADL is the linear temporal logic language XYZ/E, which can represent both dynamic and static semantics of systems as its unified formal semantic backbone. The graphical languages at the 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.