文献类型：期刊文章

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

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

出　　处：《计算机学报》

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

年　　份：2006

卷　　号：29

期　　号：4

起止页码：513-525

语　　种：中文

收录情况：BDHX、BDHX2004、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI(收录号：2006249938151)、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、核心刊

摘　　要：使用接口自动机及接口自动机网络来描述构件式系统的行为设计模型,使用UML顺序图表示基于场景的需求规约,对系统设计阶段的构件交互行为的动态兼容性进行形式化分析和检验.通过对接口自动机网络状态空间的分析,给出了一系列算法以检验系统行为的存在一致性以及几种不同形式的强制一致性性质,包括前向强制一致性、逆向强制一致性以及双向强制一致性等.

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

分 类 号：TP311]