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

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

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