软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2004年
9期
1265-1276
,共12页
蒋屹新%林闯%曲扬%尹浩
蔣屹新%林闖%麯颺%尹浩
장흘신%림틈%곡양%윤호
时序逻辑%Petri网%状态空间%模型检测
時序邏輯%Petri網%狀態空間%模型檢測
시서라집%Petri망%상태공간%모형검측
模型检测是关于系统属性验证的算法和方法.它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性.系统模型的状态空间的爆炸问题是模型检测所面临的主要问题,其主要原因是系统自身的并发特性和状态变迁的语义交织对基于Petri网的模型检测理论和验证技术进行了较为详细的研究,着重探讨了基于Petri网状态可达图的偏序简化和偏序语义技术、基于自动机的模型检测算法、基于Petri网的状态聚合法以及基于系统对称性的参数化和符号模型检测技术，并给出了研究思路以及未来所要进行的重点研究工作.模型检测技术已在通信协议和硬件系统的验证等领域得到成功应用，并且随着各种状态空间简化技术和模型检测算法的不断优化，其在其他应用领域也展示出广泛的应用前景.
模型檢測是關于繫統屬性驗證的算法和方法.它通常採用狀態空間搜索的方法來檢測一箇給定的計算模型是否滿足某箇用時序邏輯公式錶示的特定屬性.繫統模型的狀態空間的爆炸問題是模型檢測所麵臨的主要問題,其主要原因是繫統自身的併髮特性和狀態變遷的語義交織對基于Petri網的模型檢測理論和驗證技術進行瞭較為詳細的研究,著重探討瞭基于Petri網狀態可達圖的偏序簡化和偏序語義技術、基于自動機的模型檢測算法、基于Petri網的狀態聚閤法以及基于繫統對稱性的參數化和符號模型檢測技術，併給齣瞭研究思路以及未來所要進行的重點研究工作.模型檢測技術已在通信協議和硬件繫統的驗證等領域得到成功應用，併且隨著各種狀態空間簡化技術和模型檢測算法的不斷優化，其在其他應用領域也展示齣廣汎的應用前景.
모형검측시관우계통속성험증적산법화방법.타통상채용상태공간수색적방법래검측일개급정적계산모형시부만족모개용시서라집공식표시적특정속성.계통모형적상태공간적폭작문제시모형검측소면림적주요문제,기주요원인시계통자신적병발특성화상태변천적어의교직대기우Petri망적모형검측이론화험증기술진행료교위상세적연구,착중탐토료기우Petri망상태가체도적편서간화화편서어의기술、기우자동궤적모형검측산법、기우Petri망적상태취합법이급기우계통대칭성적삼수화화부호모형검측기술，병급출료연구사로이급미래소요진행적중점연구공작.모형검측기술이재통신협의화경건계통적험증등영역득도성공응용，병차수착각충상태공간간화기술화모형검측산법적불단우화，기재기타응용영역야전시출엄범적응용전경.
