基于組合形式規(guī)范的混成系統(tǒng)形式化驗證方法研究.pdf

1、混成系統(tǒng)是離散邏輯跳轉(zhuǎn)與實時連續(xù)行為交織的復雜狀態(tài)變遷系統(tǒng)，針對混成系統(tǒng)的形式化建模與驗證是確保其正確性和可靠性的重要途徑。混成系統(tǒng)不僅含有復雜的動態(tài)行為、時間限制，還包括與外部環(huán)境的通信等特征，針對混成系統(tǒng)的形式化規(guī)范技術(shù)必須能夠描述所有這些方面，但是單一的規(guī)范技術(shù)很難適合這樣的應用場景。在具體分析和驗證混成系統(tǒng)時，由于混成系統(tǒng)狀態(tài)空間是無限的，關(guān)于混成系統(tǒng)的諸多研究問題（可達性問題、模型檢測等）都是不可判定的。本文主要包括如下四個方

2、面的研究工作。
　　(1)本文基于描述系統(tǒng)行為各個方面這一想法，首先組合了三種已經(jīng)被廣泛研究的規(guī)范技術(shù)：接口自動機、多速率混成自動機和Z語言，稱為多速率混成ZIA規(guī)范，該規(guī)范不僅可以描述多速率混成系統(tǒng)軟件組件接口性質(zhì)、混成時序性質(zhì)，還具有很強的描述數(shù)據(jù)性質(zhì)的能力。
　　(2)本文給出了連續(xù)時間ZIA規(guī)范上的互模擬關(guān)系定義，不僅考慮行為間的互模擬關(guān)系，還考慮了數(shù)據(jù)間的互模擬關(guān)系；然后，基于有限論域 CT-ZIA規(guī)范，給出了其上

3、的互模擬檢測算法，并對算法正確性進行了說明。
　　(3)本文提出了針對多速率混成ZIA規(guī)范（MZIA）的帶數(shù)據(jù)約束時序邏輯，考慮到實際應用中對混成系統(tǒng)中連續(xù)變量的測量存在誤差，該邏輯可以刻畫MZIA規(guī)范“近似滿足”滿足某個給定的系統(tǒng)性質(zhì)；接下來，提出了針對多速率混成系統(tǒng)的一種近似模型檢測算法，用來判定一個MZIA規(guī)范描述的系統(tǒng)是否近似滿足某個帶數(shù)據(jù)約束的時序邏輯公式描述的性質(zhì)；最后，通過對鍋爐系統(tǒng)的例子詳細展示了MZIA規(guī)范的建模