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

Modeling and Validation of Dynamic Features of Software Architecture

作　　者：贾晓琳[1] 覃征[1] 何坚[1] 虞凡[1] 

机构地区：[1]西安交通大学电子与信息工程学院,西安710049

出　　处：《西安交通大学学报》2005年第4期347-350,355,共5页Journal of Xi'an Jiaotong University

基　　金：国家高技术研究发展计划资助项目(2003AA412020);陕西省科技发展计划"十五"攻关资助项目(2000K08 G12).

摘　　要：针对软件体系结构描述语言在分析、验证软件构架动态行为中的不足,采用谓词/变迁(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.

关 键 词：软件体系结构 谓词/变迁网 线性时序逻辑 模型验证 

分 类 号：TP302.7[自动化与计算机技术—计算机系统结构]