体系结构设计在软件开发过程中扮演着重要角色.工程中常用图形语言为软件体系结构建模,它们有直观、半形式化的优点;但是语义不够精确,难以对它们表示的模型、进行分析,在这方面,形式化方法可与之互补.但在工程使用中仅用形式化语言建模又不太现实,所以如何结合二者之长以提高软件的可靠性已成为工业界和学术界共同关心的问题.提出了双重软件体系结构描述框架XYZ/ADL:支持工程中软件体系结构的基本概念,前端用一般的体系结构框图作为结构描述,用UML活动图、状态图作为抽象行为表示;后端用既可表示系统动态语义又可表示系统静态语义的时序逻辑语言XYZ/E作为一致的语义基础.前端的图形语言便于软件工程师的交流和使用,后端的形式语言是进一步的形式化分析验证的基础.
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.