软件构架动态行为建模与检测  被引量:1

Modeling and Checking the Behavior of Software Architecture

在线阅读下载全文

作  者:何坚[1] 覃征[2] 

机构地区:[1]北京工业大学软件学院,北京100022 [2]西安交通大学电子与信息工程学院电子商务研究所,西安710049

出  处:《计算机研究与发展》2005年第11期2018-2024,共7页Journal of Computer Research and Development

基  金:国家"八六三"高技术研究发展计划基金项目(2003AA412020);陕西省"十五"科技发展计划基金项目(2000K08-G12)~~

摘  要:针对软件构架描述语言在分析、验证软件构架动态行为中的不足,用抽象代数对构件、连接器和体系结构配置进行抽象,提出了软件构架层次模型,并采用Pr/T网对软件构架动态行为建模·提出基于线性时序逻辑的软件构架动态行为模型检测方法,给出了该方法的算法描述·最后,详细描述了电子商务系统中并发控制机制的建模过程和检测结果·提出的软件构架动态行为建模与检测方法结合了Pr/T网和线性时序逻辑的优点,为开展软件构架动态行为的分析、验证提供了理论基础·Since architecture description languages are not capable enough in analyzing and validating the dynamic behavior of software architecture, the hierarchical framework for software architecture is proposed in this paper, in which the abstract algebra is used to abstract the components, connectors and architectural configuration. Meanwhile, the predicate transition (Pr/T) net is introduced to model the dynamic behavior of software architecture, and an efficient model-checking algorithm based on the linear temporal logic (LTL) is discussed in details. Finally, the approach to model a current control mechanism in an Ecommerce system and checking results based on LTL are shown in details. It can be demonstrated by practice that the modeling-and-checking method presented combines the advantages of linear temporal logic with those of Pr/T net, so that it provides novel approaches to analyze and validate the dynamic behavior of software architecture.

关 键 词:软件构架 Pr/T网 线性时序逻辑 模型检测 

分 类 号:TP311.5[自动化与计算机技术—计算机软件与理论]

 

参考文献:

正在载入数据...

 

二级参考文献:

正在载入数据...

 

耦合文献:

正在载入数据...

 

引证文献:

正在载入数据...

 

二级引证文献:

正在载入数据...

 

同被引文献:

正在载入数据...

 

相关期刊文献:

正在载入数据...

相关的主题
相关的作者对象
相关的机构对象