標題: 具時效性系統之模式化、規格與驗證之研究
Modeling,Specification and Verification of Time-Critical Systems
作者: 陳俊男
Chen Jun-Nan
謝續平
Shieh Shiuh-Pyng
資訊科學與工程研究所
關鍵字: 規格;驗證;具時效性系統;可達狀態分析;空間爆炸問題;路徑法則;Specification;Verification;Time-Critical Sys; Reachability Anal.;Space Explosion;Path Approach
公開日期: 1993
摘要: 本文旨在探討如何將具時效性系統加以模式化,藉由本文所提出之模型 :時間化之傳輸有限狀態機,我們可以將一個具時效性系統加以規格,並利 用所得之規格,驗證系統的時效性是否正確,我們所採用的方法乃是屬於可 達狀態分析的一種, 為了解決可達狀態分析所為人垢病的空間爆炸問題, 我們又提出一種以路徑法則為基礎的改良演算法,並且證明該法的空間複 雜度確實較傳統的可達狀態分析來得小.最後,我們也提出了目前著手工作 概況與未來研究之方向,作為本文之結束. In this paper, we propose a new formalism named the Timed Communi cating Finite State Machine (Timed CFSM) for specifying and verif ying time-critical systems. A given time-dependent specification can be formalized as a Timed CFSM, from which the reachability gr aph is constructed to verify the correctness of the specification . We also propose a new algorithm to resolve the space explosion problem from which the reachability graph suffers.
URI: http://140.113.39.130/cdrfb3/record/nctu/#NT820392057
http://hdl.handle.net/11536/57864
顯示於類別:畢業論文