《软件构架动态行为建模与检测》由会员分享，可在线阅读，更多相关《软件构架动态行为建模与检测（7页珍藏版）》请在金锄头文库上搜索。
1、计算机研究与发展ISSN 100021239/ CN 1121777/ TP Journal of Computer Research and Development42(11) : 20182024 , 2005收稿日期:2004-05-20 ;修回日期:2004-05-23基金项目:国家 “八六三” 高技术研究发展计划基金项目(2003AA412020) ;陕西省 “十五” 科技发展计划基金项目(2000K082G12)软件构架动态行为建模与检测何 坚1 ,2覃 征21(北京工业大学软件学院 北京 100022) 2(西安交通大学电子与信息工程学院电子商务研究所 西安 710049)(Ji
2、anhee 1631com)Modeling and Checking the Behavior of Software ArchitectureHe Jian1 ,2and Qin Zheng21( School of Sof tware Engineering , Beijing University of Technology , Beijing100022)2( E2Commerce Institute, School of Electronic and Information Engineering , Xian Jiaotong University , Xian710049)Ab
3、stract Since architecture description languages are not capable enough in analyzing and validating thedynamic behavior of software architecture , the hierarchical framework for software architecture isproposedin this paper , in which the abstract algebra is used to abstract the components , connecto
4、rs and architecturalconfiguration1Meanwhile , the predicate transition (PrT) net is introduced to model the dynamic behaviorof software architecture , and an efficient model2checking algorithm based on the linear temporal logic (L TL) is discussed in details1Finally , the approach to model a current
5、 control mechanism in an E2com2merce system and checking results based on L TL are shown in details1It can be demonstrated by practicethat the modeling2and2checking method presented combines the advantages of linear temporal logic withthose of PrT net , so that it provides novel approaches to analyz
6、e and validate the dynamic behavior of soft2ware architecture1Key words software architecture ; PrT net ; linear temporal logic; model checking摘 要 针对软件构架描述语言在分析、 验证软件构架动态行为中的不足,用抽象代数对构件、 连接器和 体系结构配置进行抽象,提出了软件构架层次模型,并采用PrT网对软件构架动态行为建模1 提出基 于线性时序逻辑的软件构架动态行为模型检测方法,给出了该方法的算法描述1 最后,详细描述了电子 商务系统中并发控制机制的建模
7、过程和检测结果1 提出的软件构架动态行为建模与检测方法结合了PrT网和线性时序逻辑的优点,为开展软件构架动态行为的分析、 验证提供了理论基础1关键词 软件构架;PrT网;线性时序逻辑;模型检测中图法分类号 TP311151 引 言软件构架是对系统整体组织结构和控制结构的 刻画1 它包括系统中各计算单元(构件)的功能分 配,各单元之间的高层交互(连接器)说明,以及软件构架的约束11 目前软件构架的研究主要集中在软件构架描述语言(architecture description language ,ADL)方面1ADL只关心软件系统的高层结构,不关心具体 的软件实现细节,是对软件构架的形式化描述1
8、 研 究人员基于不同形式化建模技术已开发了多种ADL1 例 如, Allen采 用CSP开 发 了Wright2,Kramer等人基于 2演算设计实现了Darwin3,中科院软件所采用时序逻辑设计了XYZADL4等1 这些ADL针对软件构架的不同风格引入特定符号 和公理描述软件构架的静态结构和构件交互,它们 具有规范的语法和严格的语义,为软件构架实践提 供了指导1 但是大型分布式软件系统包含大量并发运行的构件,构件之间存在复杂的相互通信与制约 关系,已有ADL在描述软件构架动态行为时表达不 直观,缺少可视化、 自动化的软件构架动态行为分析 验证工具,使得设计人员难以在系统设计的早期阶 段分析、
9、 测试系统的正确性、 适应性1谓词 变迁网(predicate transition nets ,PrT网) 作为一种高级Petri网5,能简洁地描述系统的动态 特性1 它不但提供可视的图形表示,还具有强大完 整的数学基础和分析方法,被广泛地应用在具有并 发、 并行、 异步和随机性质的系统建模与分析中1 因此,本文提出了基于PrT网的软件构架动态行为建 模方法1 为了确保软件构架动态行为模型(behaviormodel of software architecture ,BM)可靠、 符合实际, 本文提出了基于线性时序逻辑(linear temporal log2ic ,L TL)的BM模型检
10、测方法1 该方法首先用L TL公式定义软件构架动态行为规约;再将L TL公式转 化成等价的Bchi自动机6;最后,通过构造BM模 型的可达图和Bchi自动机的同步积来分析、 检测BM模型的正确性12 软件构架动态行为建模软件构架是一种基于构件的思想,它从系统的 总体结构入手,将系统分解为构件和构件之间的交 互关系1 在实际开发过程中,研究人员针对不同应用领域开发了多种ADL ,Medvidovic和Taylor通过 分析、 比较这些ADL ,认为一个软件构架包括构件、 连接器、 体系结构配置71211 软件构架分层模型 大型软件系统通常包括大量构件,其中的复杂成员构件可由简单的低层构件集成而成
11、1 因此,若 将软件系统本身作为一个构件,则可得到软件构架 的层次模型(hierarchical architectural mode ,HAM)1 借鉴CBSD和中间件技术有关构件和接口定义,HAM可定义如下:HAM=构件规约,连接器规约,体系结构配 置规约 构件规约 =构件结构规约,构件接口规约 构件结构规约 =原子构件结构|复合构件结构 原子构件结构 =构件标识,构件实现的 引用复合构件结构 =引用的构件类型,实例声 明,实例连接,映射构件接口规约 =所属构件的标识,端口规约,服务集合 服务集合 =对外提供的功能集合,对外请求的功能集合 端口规约 =所属构件标识,行为规约,行为模型连接器
12、规约 =连接器标识,连接器约束 体系结构配置规约 =实例声明,实例连接,实例连接约束HAM模型具有以下性质: (1)一个软件系统由构件和连接器组成,体系结构配置规约定义了构件通过连接器实现与外部环 境交互的约束条件1 (2)构件规约包括接口部分和结构部分,接口的服务集合定义了构件对外提供(或需求)的功能和 服务1 端口规约定义了构件的动态行为特征,即构 件与外部环境的交互信息1 (3)原子构件的结构部分定义了对构件实现的引用1 复合构件的结构部分定义了成员构件之间的 连接关系,具体包括引用的成员构件的类型、 成员构 件实例、 实例之间的连接关系以及复合构件接口规 约向成员构件接口规约的映射1
13、(4) HAM支持对软件构架进行纵向、 横向的分解,即纵向看一个HAM模型包含许多层,每一层是 对上层复合构件的细化,因此,HAM支持软件构架 自顶向下和自底向上的设计方法;横向看HAM模 型每层由多个构件和连接器构成,构件只能通过端 口与外部环境进行交互1 在HAM模型中,构件的状态及其行为被构件 接口所封装,连接器将存在交互关系的两构件端口 连接起来,并通过连接器约束定义交互的约束条件1 基于HAM模型,我们开发了基于构件的分布式软 件构架描述语言(DSADL)81212 BM模型定义HAM模型引入端口概念,实现了构件的计算 功能与交互功能分离,为构架动态行为建模、 分析提 供了基础1 设
14、计人员对软件构架动态行为建模时, 只需考虑构件端口和连接器的交互行为,而不用考 虑构件的功能及算法实现1 由于PrT网能简洁地 描述系统的并发、 同步、 冲突等动态特性,因此本文9102何 坚等:软件构架动态行为建模与检测对DSADL进行扩充,采用PrT网建立BM模型1 定义11BM模型是对PrT网的扩展,其形式 化定义为: BM =( IC , Sports , Scons , Cnet , Af,Child)1 其中:IC为构件的惟一标识符1Sports是构件所含端口的集合,即 port1,port2, portn ,而每个porti=id , params , f ace ,cons 1
15、 其中, id是端口的惟一标识符; params为端 口的输入、 输出参数说明; f ace为端口的外观表示, 在DSADL中端口用圆圈表示1cons是端口行为的 约束条件1Scons是构件所含连接器的集合,即 connector1,connector2, connectorn ,每个connectori=id ,type, f ace , cons 1 其中, id是连接器的惟一标识 符; type是服务类型,表示连接器所连端口提供服 务的方向; f ace为连接器的外观表示,在DSADL中 连接器用有向线段表示1cons是连接器约束的集合, 它包括连接器的初始条件、 前置条件和后置条件1C
16、net是一PrT网,用来描述构件端口的交互 行为和限制条件1PrT网定义参见文献51Af是一个函数映射1 其中,将构件端口映射为PrT网中的库所;将构件端口的行为约束和连接器 约束集映射为变迁;依据连接器类型将连接器映射 为PrT网中的有向弧,并根据端口的参数说明生成PrT网中的弧标记1Child为子类BM模型的惟一标识符,若不存 在子类BM模型,则Child为空1 为了支持软件构架动态行为分层建模,本文对Cnet中的库所进行了分类1 定义21BM模型中的库所定义为place=( Pid ,Type , Subnet) ,其中:Pid表示库所的惟一标志1Type是库所的类型1BM模型中有两类库所, 其中, PP为原子库所,表示在系统的任意抽象层次 都不可细化; A P为抽象库所,表示在系统建模过程 中,可以进一步细化1Subnet是库所细化模型的惟一标识符;如果库 所没
