软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2006年
1期
48-58
,共11页
胡军%于笑丰%张岩%李宣东%郑国梁
鬍軍%于笑豐%張巖%李宣東%鄭國樑
호군%우소봉%장암%리선동%정국량
实时软件%构件式设计%模型检验%接口自动机%顺序图%统一建模语言
實時軟件%構件式設計%模型檢驗%接口自動機%順序圖%統一建模語言
실시연건%구건식설계%모형검험%접구자동궤%순서도%통일건모어언
在复杂的实时软件系统中使用构件式设计方法,已成为目前软件工程中的研究热点.如何有效地验证实时软件的设计是否满足给定的时间规约,是实时计算领域中的主要挑战之一.通过在接口自动机模型中添加时间区间标记,来扩展其对实时系统接口行为的表达能力;使用实时接口自动机网络来描述实时软件系统的构件式设计模型;使用带布尔不等式时间约束的UML顺序图表示基于场景的需求规约,对系统设计阶段实时软件构件的动态行为进行形式化分析与检验.通过对实时接口自动机网络状态空间的分析,构造了其可兼容的整型状态等价类空间的可达图,并在此基础上给出了验证算法,以检验构件式实时软件系统的设计与带时间约束的场景式规约之间的一致性.
在複雜的實時軟件繫統中使用構件式設計方法,已成為目前軟件工程中的研究熱點.如何有效地驗證實時軟件的設計是否滿足給定的時間規約,是實時計算領域中的主要挑戰之一.通過在接口自動機模型中添加時間區間標記,來擴展其對實時繫統接口行為的錶達能力;使用實時接口自動機網絡來描述實時軟件繫統的構件式設計模型;使用帶佈爾不等式時間約束的UML順序圖錶示基于場景的需求規約,對繫統設計階段實時軟件構件的動態行為進行形式化分析與檢驗.通過對實時接口自動機網絡狀態空間的分析,構造瞭其可兼容的整型狀態等價類空間的可達圖,併在此基礎上給齣瞭驗證算法,以檢驗構件式實時軟件繫統的設計與帶時間約束的場景式規約之間的一緻性.
재복잡적실시연건계통중사용구건식설계방법,이성위목전연건공정중적연구열점.여하유효지험증실시연건적설계시부만족급정적시간규약,시실시계산영역중적주요도전지일.통과재접구자동궤모형중첨가시간구간표기,래확전기대실시계통접구행위적표체능력;사용실시접구자동궤망락래묘술실시연건계통적구건식설계모형;사용대포이불등식시간약속적UML순서도표시기우장경적수구규약,대계통설계계단실시연건구건적동태행위진행형식화분석여검험.통과대실시접구자동궤망락상태공간적분석,구조료기가겸용적정형상태등개류공간적가체도,병재차기출상급출료험증산법,이검험구건식실시연건계통적설계여대시간약속적장경식규약지간적일치성.
