基于時間自動機的實時系統(tǒng)規(guī)范驗證研究.pdf

1、實時系統(tǒng)不僅要求邏輯上是正確的,而且要求時間上也是正確的,這類系統(tǒng)在設(shè)計階段需要進行嚴格的分析和驗證.時間自動機是使用最為廣泛的對實時系統(tǒng)進行規(guī)范驗證的形式化方法之一.實時系統(tǒng)驗證主要分為安全性驗證和活性驗證,系統(tǒng)的活性可以通過位置的不變式和轉(zhuǎn)移的約束條件保證,驗證也比較容易,本文對此不作過多討論.安全性驗證問題可歸結(jié)為時間自動機的可達性分析,基于狀態(tài)空間搜索的方法主要不足在于狀態(tài)空間的大小隨著過程數(shù)目的增加呈指數(shù)級遞增,這就導致了狀態(tài)

2、空間爆炸問題.為了解決這個問題,我們必須構(gòu)造時間自動機狀態(tài)空間的有窮表示.本文主要研究了Alur提出的域自動機方法、帶自動機方法以及Inhye Kang等提出的狀態(tài)空間最小化方法,并在此基礎(chǔ)上提出了時間段轉(zhuǎn)換系統(tǒng)以及對狀態(tài)空間的極小化方法.該方法用位置和進入位置的最大最小時鐘值集合來表示狀態(tài)而得到時間段轉(zhuǎn)換系統(tǒng),同時通過轉(zhuǎn)換分析保留有效轉(zhuǎn)換來簡化這個轉(zhuǎn)換系統(tǒng).對簡化后的系統(tǒng),使用轉(zhuǎn)換互模擬進行最小化.文中對該方法進行了可行性分析,通過與