基于场景规约的构件式系统设计分析与验证  

Checking Component-Based Designs for Scenario-Based Specifications

作　　者：胡军[1] 于笑丰[2] 张岩[1] 王林章[1] 李宣东[1] 郑国梁[1] 

机构地区：[1]计算机软件新技术国家重点实验室,南京210093 [2]南京大学计算机科学与技术系,南京210093

出　　处：《计算机学报》2006年第4期513-525,共13页Chinese Journal of Computers

基　　金：国家自然科学基金(60425204;60233020;60573085);国家"九七三"重点基础研究发展规划项目基金(2002CB312001);江苏省自然科学基金(BK2004080)资助

摘　　要：使用接口自动机及接口自动机网络来描述构件式系统的行为设计模型,使用UML顺序图表示基于场景的需求规约,对系统设计阶段的构件交互行为的动态兼容性进行形式化分析和检验.通过对接口自动机网络状态空间的分析,给出了一系列算法以检验系统行为的存在一致性以及几种不同形式的强制一致性性质,包括前向强制一致性、逆向强制一致性以及双向强制一致性等.Component-based system design is becoming more and more popular in software engineering. Checking the important behavioral properties formally in the design phase is an effective way to improve the system reliability. In this paper, the authors consider the problem of checking component-based system designs for scenario-based specifications. Specifically, the authors use the interface automata networks to model the component-based system designs which include a set of interface automata synchronized by shared actions, and the scenario-based specifications are specified by UML sequence diagrams. Based on investigating the reachability graph of the state space of the interface automata networks, the authors develop several algorithms to check the existential consistency and mandatory consistency including the forward, backward and bidirectional consistency.

关 键 词：构件式系统设计 接口自动机 模型检验 顺序图 统一建模语言(UML) 

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