小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2012年
2期
219-224
,共6页
构件系统%时间接口%时间接口自动机%验证
構件繫統%時間接口%時間接口自動機%驗證
구건계통%시간접구%시간접구자동궤%험증
在复杂的实时系统开发中使用构件式设计方法已成为目前软件开发领域中的研究热点,如何有效地验证实时软件的设计是否满足给定的时间需求并降低验证过程的复杂度,是实时计算领域中的主要挑战之一.文中对构件接口模型进行时间扩展,提出了时间接口模型,并将其用于构件接口交互行为的形式化建模.在接口自动机理论的的基础上进一步提出了时间接口自动机模型用于描述时间接口交互下构件的行为及组合方法,通过消除错误状态产生组合模型来约减构件时间接口自动机模型的积,并在约减的模型上进行性质检验,降低了分析复杂度,有效地应对状态空间爆炸问题.为了说明论文建议的方法,详细讨论了一个简单的、贯穿整篇论文的示例系统.
在複雜的實時繫統開髮中使用構件式設計方法已成為目前軟件開髮領域中的研究熱點,如何有效地驗證實時軟件的設計是否滿足給定的時間需求併降低驗證過程的複雜度,是實時計算領域中的主要挑戰之一.文中對構件接口模型進行時間擴展,提齣瞭時間接口模型,併將其用于構件接口交互行為的形式化建模.在接口自動機理論的的基礎上進一步提齣瞭時間接口自動機模型用于描述時間接口交互下構件的行為及組閤方法,通過消除錯誤狀態產生組閤模型來約減構件時間接口自動機模型的積,併在約減的模型上進行性質檢驗,降低瞭分析複雜度,有效地應對狀態空間爆炸問題.為瞭說明論文建議的方法,詳細討論瞭一箇簡單的、貫穿整篇論文的示例繫統.
재복잡적실시계통개발중사용구건식설계방법이성위목전연건개발영역중적연구열점,여하유효지험증실시연건적설계시부만족급정적시간수구병강저험증과정적복잡도,시실시계산영역중적주요도전지일.문중대구건접구모형진행시간확전,제출료시간접구모형,병장기용우구건접구교호행위적형식화건모.재접구자동궤이론적적기출상진일보제출료시간접구자동궤모형용우묘술시간접구교호하구건적행위급조합방법,통과소제착오상태산생조합모형래약감구건시간접구자동궤모형적적,병재약감적모형상진행성질검험,강저료분석복잡도,유효지응대상태공간폭작문제.위료설명논문건의적방법,상세토론료일개간단적、관천정편논문적시례계통.
