一種基于時間自動機的域構造方法
2005-04-29 00:00:00錢俊彥趙嶺忠
計算機應用研究 2005年7期
摘 要：模型檢驗是一種重要的形式化自動驗證技術，通過狀態(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
