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

被引:40
作者
胡军 [1 ]
于笑丰 [2 ]
张岩 [1 ]
王林章 [1 ]
李宣东 [1 ]
郑国梁 [1 ]
机构
[1] 计算机软件新技术国家重点实验室
[2] 南京大学计算机科学与技术系
关键词
构件式系统设计; 接口自动机; 模型检验; 顺序图; 统一建模语言(UML);
D O I
暂无
中图分类号
TP311.52 [];
学科分类号
081202 ; 0835 ;
摘要
使用接口自动机及接口自动机网络来描述构件式系统的行为设计模型,使用UML顺序图表示基于场景的需求规约,对系统设计阶段的构件交互行为的动态兼容性进行形式化分析和检验.通过对接口自动机网络状态空间的分析,给出了一系列算法以检验系统行为的存在一致性以及几种不同形式的强制一致性性质,包括前向强制一致性、逆向强制一致性以及双向强制一致性等.
引用
收藏
页码:4513 / 4525
页数:13
相关论文
共 1 条
[1]   LSCs: Breathing life into message sequence charts [J].
Damm, W ;
Harel, D .
FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (01) :45-80