Research on Formal Specification of Software Architecture Based on Temporal Logic
基于时序逻辑软件构架形式化方法研究

Development based on software architecture is one of the most effective solutions to improve software quality and productivity, and minimize the difficulties of developing large and complex systems. Formal models and specifications of software architecture are one of the key research areas of software architecture. In this paper, the extension of XYZ/E Language based on set theory, called XYZ/E+ Language, is proposed, and a method of formalizing software architecture whit it is formulated. The formal method is distinguished by its ability to represent not only static properties but also dynamic behaviors, and its high-level abstraction and powerful expressiveness. Finally, through an example of formalizing software architecture of a specific system with XYZ/E + Language, its powerful modeling ability and good practicality are demonstrated.