软件体系结构动态特征建模与验证

Modeling and Validation of Dynamic Features of Software Architecture

针对软件体系结构描述语言在分析、验证软件构架动态行为中的不足,采用谓词/变迁(Pr/T)网为软件体系结构动态行为建模,并提出了基于线性时序逻辑的软件体系结构动态行为模型验证方法.首先根据体系结构层次模型扩展Pr/T网建立体系结构动态行为模型(DFM)并构造DFM的可达图,然后使用基于自动机理论的方法来验证模型的时态逻辑性质,最后通过对一个电子商务系统实例的并发控制机制建模和模型检测,验证了该方法的有效性.所提方法结合了Pr/T网和线性时序逻辑的优点,为进一步开展软件体系结构动态行为的分析、验证奠定了基础.

Due to the deficiency of architecture description languages in analyzing and validating dynamic behavior of software systems, the predicate/transition (Pr/T) net was introduced to model the dynamic features of software architecture, and an efficient model-checking algorithm was proposed. Firstly, the dynamic feature model (DFM) of the architecture was constructed in terms of extended Pr/T net of the hierarchical model of it and the approachability graph was formed. Then the linear temporal logic properties (LTL) of the system could be verified based on the model checking method of automata theory. Finally, the validity of our approach was shown through modelling the concurrent control system and checking model in a case study of an electronic commerce system. It is demonstrated by the practice that the modelling-and-checking method presented combines the advantages of linear temporal logic with those of Pr/T net, so that it provides a basis for further developing approaches to analyze and validate dynamic features of software architectures.