计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2006年
4期
513-525
,共13页
胡军%于笑丰%张岩%王林章%李宣东%郑国梁
鬍軍%于笑豐%張巖%王林章%李宣東%鄭國樑
호군%우소봉%장암%왕림장%리선동%정국량
构件式系统设计%接口自动机%模型检验%顺序图%统一建模语言(UML)
構件式繫統設計%接口自動機%模型檢驗%順序圖%統一建模語言(UML)
구건식계통설계%접구자동궤%모형검험%순서도%통일건모어언(UML)
使用接口自动机及接口自动机网络来描述构件式系统的行为设计模型,使用UML顺序图表示基于场景的需求规约,对系统设计阶段的构件交互行为的动态兼容性进行形式化分析和检验.通过对接口自动机网络状态空间的分析,给出了一系列算法以检验系统行为的存在一致性以及几种不同形式的强制一致性性质,包括前向强制一致性、逆向强制一致性以及双向强制一致性等.
使用接口自動機及接口自動機網絡來描述構件式繫統的行為設計模型,使用UML順序圖錶示基于場景的需求規約,對繫統設計階段的構件交互行為的動態兼容性進行形式化分析和檢驗.通過對接口自動機網絡狀態空間的分析,給齣瞭一繫列算法以檢驗繫統行為的存在一緻性以及幾種不同形式的彊製一緻性性質,包括前嚮彊製一緻性、逆嚮彊製一緻性以及雙嚮彊製一緻性等.
사용접구자동궤급접구자동궤망락래묘술구건식계통적행위설계모형,사용UML순서도표시기우장경적수구규약,대계통설계계단적구건교호행위적동태겸용성진행형식화분석화검험.통과대접구자동궤망락상태공간적분석,급출료일계렬산법이검험계통행위적존재일치성이급궤충불동형식적강제일치성성질,포괄전향강제일치성、역향강제일치성이급쌍향강제일치성등.
