摘 要:模型檢驗是一種重要的形式化自動驗證技術,通過狀態(tài)空間搜索來保證軟硬件設計的正確性。由于 TCTL不是針對時間自動機,而是針對有限狀態(tài)變遷系統(tǒng)的,從而無法使用TCTL直接對時間自動機進行模型檢驗。給出了一種從時間自動機到有限狀態(tài)變遷系統(tǒng)的方法,并在不改變時間自動機的語義上,使時間自動機等價后的域狀態(tài)數盡可能少,在一定程度上有效地解決了狀態(tài)空間爆炸問題。
關鍵詞:模型檢驗;時間自動機;TCTL
中圖法分類號:TP301
文獻標識碼:A
文章編號:1001—3695(2005)07—0068—03