具時效性系統之模式化、規格與驗證之研究

Abstract

本文旨在探討如何將具時效性系統加以模式化,藉由本文所提出之模型 :時間化之傳輸有限狀態機,我們可以將一個具時效性系統加以規格,並利 用所得之規格,驗證系統的時效性是否正確,我們所採用的方法乃是屬於可 達狀態分析的一種, 為了解決可達狀態分析所為人垢病的空間爆炸問題, 我們又提出一種以路徑法則為基礎的改良演算法,並且證明該法的空間複 雜度確實較傳統的可達狀態分析來得小.最後,我們也提出了目前著手工作 概況與未來研究之方向,作為本文之結束. 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.