混合系統(tǒng)的形式化驗證.pdf

1、混合系統(tǒng)是連續(xù)變量和離散事件非平凡混合的計算系統(tǒng)，典型的例子有空中交通管制，汽車控制，機器人，載人航天等等。特別是對安全性要求極高的應用領域，混合系統(tǒng)的形式化驗證逐漸成為一種保證系統(tǒng)正確性的重要方法?；旌舷到y(tǒng)的形式化驗證主要包括定理證明和模型檢查。其中，可達性分析是模型檢查的基礎。 由于混合系統(tǒng)是無窮狀態(tài)空間上的復雜系統(tǒng)，目前關于混合系統(tǒng)的模型檢查問題的研究還集中在可達性分析領域。因為即便是可達性問題，也只有很小的一類混合系統(tǒng)子

2、集(矩形混合系統(tǒng))是可判定的。對于混合系統(tǒng)的可達性問題，大多數(shù)研究者都采用普通多面體或類似于普通多面體的結(jié)構(gòu)來表示狀態(tài)集，用量詞消去運算計算可達集。量詞消去運算的計算復雜度是雙指數(shù)級的。對于混合系統(tǒng)模型檢查問題的研究，還集中在實時系統(tǒng)(可以看作是最簡單的混合系統(tǒng))領域。本文主要包含如下四個方面的工作。 首先解決了有界整數(shù)域上的一階投影時序邏輯的可滿足性問題。同時，定義了一種基于稠密時間的時間區(qū)間時序邏輯來描述實時和混合系統(tǒng)的性質(zhì)

3、。通過轉(zhuǎn)換為有界整數(shù)域上一階投影時序邏輯的可滿足性問題，證明了稠密的時間區(qū)間時序邏輯的可滿足性問題是可判定的。 提出了一種稱作混合區(qū)域的約束系統(tǒng)，它可用于矩形混合系統(tǒng)的符號化可達性分析?；旌蠀^(qū)域是由滿足嚴格限制條件的線性不等式聯(lián)立表示的多面體區(qū)域。這些線性不等式都由一個線性表達式和一個有理數(shù)通過不等號連接而成，其中線性表達式中的變量不超過兩個，并且變量的系數(shù)與混合系統(tǒng)中相應斜率的取值范圍有關。使用混合區(qū)域進行矩形混合系統(tǒng)可達性分

4、析，必須保證其對于矩形自動機可達性操作的封閉性。本文用了很大篇幅證明了混合區(qū)域?qū)τ诰匦巫詣訖C兩種類型的轉(zhuǎn)換操作是封閉的，即一個混合區(qū)域經(jīng)過一個延遲轉(zhuǎn)換，或一個跳躍轉(zhuǎn)換后所有可達的狀態(tài)仍可用一個混合區(qū)域來表示。為了在計算機中存儲混合區(qū)域，我們定義了一種稱作不同上限矩陣的矩陣數(shù)據(jù)結(jié)構(gòu)。把不同上限矩陣轉(zhuǎn)換為標準型之后，矩形混合系統(tǒng)的可達性運算就變得很直接。這樣，使用不同上限矩陣進行矩形混合系統(tǒng)的可達性分析，主要的運算就是計算標準型。而標準型問

5、題是線性優(yōu)化問題，可以利用多項式復雜度的算法加以解決。我們還定義了一種稱作矩形混合圖表的結(jié)構(gòu)處理混合區(qū)域的并。此外，我們還介紹的一種用矩形自動機近似模擬非線性混合系統(tǒng)的方法，然后使用混合區(qū)域判定矩形自動機的可達性問題進而近似地判定非線性混合系統(tǒng)的可達性問題。 提出了多速率混合系統(tǒng)的一種模型檢查算法，用來判定一個多速率自動機M描述的系統(tǒng)是否滿足某個稠密的時間區(qū)間時序邏輯公式φ描述的性質(zhì)。我們定義了多速率自動機賦值集上的一種等價關系