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

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

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

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