计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2006年
5期
287-289
,共3页
模型检测%Spin%Promela%Petri网%线性时序逻辑
模型檢測%Spin%Promela%Petri網%線性時序邏輯
모형검측%Spin%Promela%Petri망%선성시서라집
Petri网是描述并发系统的很直观的图形工具;Spin是一种著名的分析验证并发系统性质的工具.本文首先论述Petri网性质的线性时序逻辑描述,研究用Promela编程描述Petri网和用Spin对Petri网性质进行检验的方法,最后通过两个具体的示例说明这种方法是成功的.
Petri網是描述併髮繫統的很直觀的圖形工具;Spin是一種著名的分析驗證併髮繫統性質的工具.本文首先論述Petri網性質的線性時序邏輯描述,研究用Promela編程描述Petri網和用Spin對Petri網性質進行檢驗的方法,最後通過兩箇具體的示例說明這種方法是成功的.
Petri망시묘술병발계통적흔직관적도형공구;Spin시일충저명적분석험증병발계통성질적공구.본문수선논술Petri망성질적선성시서라집묘술,연구용Promela편정묘술Petri망화용Spin대Petri망성질진행검험적방법,최후통과량개구체적시례설명저충방법시성공적.