苏州大学学报（工科版）
囌州大學學報（工科版）
소주대학학보（공과판）
JOURNAL OF SOOCHOW UNIVERSITY ENGINEERING SCIENCE EDITION
2005年
2期
1-6
,共6页
模型检测%实时系统%时间自动机%域自动机%时序逻辑
模型檢測%實時繫統%時間自動機%域自動機%時序邏輯
모형검측%실시계통%시간자동궤%역자동궤%시서라집
模型检测是一种用于并发系统性质验证的算法技术.实际生活中广泛应用的是带有时间约束的并发系统即实时系统,现在模型检测技术越来越被广泛地应用到这类系统的性质验证当中.这类系统通常用时间自动机来表示,而它们的性质则用时序逻辑公式表示.本文简要介绍了时间自动机和时序逻辑TCTL,并着重说明了如何进行基于稠密时间的实时系统的模型检测,最后给出了一个应用实例.
模型檢測是一種用于併髮繫統性質驗證的算法技術.實際生活中廣汎應用的是帶有時間約束的併髮繫統即實時繫統,現在模型檢測技術越來越被廣汎地應用到這類繫統的性質驗證噹中.這類繫統通常用時間自動機來錶示,而它們的性質則用時序邏輯公式錶示.本文簡要介紹瞭時間自動機和時序邏輯TCTL,併著重說明瞭如何進行基于稠密時間的實時繫統的模型檢測,最後給齣瞭一箇應用實例.
모형검측시일충용우병발계통성질험증적산법기술.실제생활중엄범응용적시대유시간약속적병발계통즉실시계통,현재모형검측기술월래월피엄범지응용도저류계통적성질험증당중.저류계통통상용시간자동궤래표시,이타문적성질칙용시서라집공식표시.본문간요개소료시간자동궤화시서라집TCTL,병착중설명료여하진행기우주밀시간적실시계통적모형검측,최후급출료일개응용실례.
