形式驗證技術(shù)中流管道近似方法的研究與應(yīng)用.pdf

1、混合系統(tǒng)是連續(xù)動態(tài)過程和離散事件動態(tài)過程并存，且相互影響、相互作用的一類動態(tài)系統(tǒng)。八十年代后期，隨著微型計算機、大型通訊網(wǎng)和微處理器在控制領(lǐng)域的大量應(yīng)用，混合系統(tǒng)廣泛出現(xiàn)于生產(chǎn)實際中，混合系統(tǒng)成為自動控制和計算機理論兩大領(lǐng)域的研究熱點。 論文首先介紹了混合系統(tǒng)的概念和一些混合系統(tǒng)的典型實例，針對混合系統(tǒng)的建模、分析、驗證方法作了系統(tǒng)的闡述。詳細(xì)介紹了混合系統(tǒng)形式驗證的研究現(xiàn)狀、驗證工具和基木概念。 針對混合系統(tǒng)既包含連續(xù)

2、動態(tài)過程又包含離散事件過程的特點，研究了通過混合自動機模型進行混合系統(tǒng)建模的方法；對于混合系統(tǒng)驗證中的模型檢驗問題，分析了計算樹邏輯CTL和基于動作的時序邏輯ACTL。 對可達集的表示和計算方法進行了較為深入的研究：對比了使用凸多面體、超矩形和有向矩形殼表示可達集時，在過近似的保守性，計算的復(fù)雜度，集合交、并處理能力和維數(shù)增長時凸多面體頂點和面的增長速度等方面的優(yōu)劣。在此基礎(chǔ)上，歸納出了可達集的表示和計算方法的選用原則。

3、 流管道的近似方法是形式驗證技術(shù)的一個重要內(nèi)容。根據(jù)混合系統(tǒng)中的連續(xù)部分的動態(tài)特性，可將混合系統(tǒng)分為時鐘型、線性和非線性三種類型。對于不同類型的混合系統(tǒng)，其流管道近似方法都不相同。本文針對這三種類型的混合系統(tǒng)，詳細(xì)分析了各個類型混合系統(tǒng)的流管道近似方法，并分別對濃度控制系統(tǒng)(時鐘型)、化工蒸發(fā)過程(非線性)和常壓爐加熱系統(tǒng)(線性)作為形式驗證的對象，對它們的連續(xù)動態(tài)和離散動態(tài)部分分析的基礎(chǔ)上，建立混合自動機模型，提出需要驗證的形式規(guī)范，