基于可達(dá)集過近似的混合系統(tǒng)驗(yàn)證方法.pdf

1、混合系統(tǒng)是連續(xù)變量過程和離散事件過程并存,且相互交換信息的一類動(dòng)態(tài)系統(tǒng).八十年代后期,隨著微型計(jì)算機(jī)、大型通訊網(wǎng)和微處理器在控制領(lǐng)域的大量應(yīng)用,一批反映先進(jìn)技術(shù)發(fā)展方向的人造系統(tǒng)大量涌現(xiàn),連續(xù)動(dòng)態(tài)過程與離散事件混合的系統(tǒng)廣泛出現(xiàn)于生產(chǎn)實(shí)際中,混合系統(tǒng)成為自動(dòng)控制和計(jì)算機(jī)理論兩大領(lǐng)域的研究熱點(diǎn). 論文首先回顧了混合系統(tǒng)的產(chǎn)生背景,介紹了混合系統(tǒng)的概念、特點(diǎn)、研究意義及發(fā)展現(xiàn)狀,重點(diǎn)介紹了混合系統(tǒng)的形式化驗(yàn)證方法,分析了系統(tǒng)仿真與形

2、式化驗(yàn)證的異同,對(duì)現(xiàn)有的基于模型檢驗(yàn)的混合系統(tǒng)形式化驗(yàn)證工具進(jìn)行了對(duì)比與分析. 針對(duì)混合系統(tǒng)既包含連續(xù)動(dòng)態(tài)過程又包含離散事件過程的特點(diǎn),研究了通過混合自動(dòng)機(jī)模型進(jìn)行混合系統(tǒng)建模的方法;對(duì)于混合系統(tǒng)驗(yàn)證中的模型檢驗(yàn)問題,分析了計(jì)算樹邏輯CTL和基于動(dòng)作的時(shí)序邏輯ACTL. 對(duì)可達(dá)集的表示和計(jì)算方法進(jìn)行了較為深入的研究:對(duì)比了使用凸多面體、超矩形和有向矩形殼表示可達(dá)集時(shí),在過近似的保守性,計(jì)算的復(fù)雜度,集合交、并處理能力和維

3、數(shù)增長(zhǎng)時(shí)凸多面體頂點(diǎn)和面的增長(zhǎng)速度等方面的優(yōu)劣.在此基礎(chǔ)上,歸納出了可達(dá)集的表示和計(jì)算方法的選用原則. 研究了基于可達(dá)集近似和切換面劃分的混合系統(tǒng)驗(yàn)證方法,包括:初始劃分、可達(dá)集近似、遷移關(guān)系的確定以及當(dāng)出現(xiàn)不可決策狀況時(shí)的細(xì)劃分等.提出了通過頂點(diǎn)仿真與可達(dá)集近似相結(jié)合的遷移關(guān)系簡(jiǎn)化算法:針對(duì)線性定常系統(tǒng)的特點(diǎn),結(jié)合凸多面體的性質(zhì),給出了在連續(xù)狀態(tài)方程為線性定常的不變集內(nèi),當(dāng)初始區(qū)域?yàn)橥苟嗝骟w時(shí)系統(tǒng)可達(dá)集的演化規(guī)律,并加以證明.

4、依據(jù)這些結(jié)論,對(duì)混合系統(tǒng)形式驗(yàn)證中遷移關(guān)系的計(jì)算方法進(jìn)行了簡(jiǎn)化,并給出了計(jì)算過程與程序?qū)崿F(xiàn)框圖. 根據(jù)文中提出的方法,結(jié)合實(shí)例編寫了驗(yàn)證程序,實(shí)現(xiàn)了驗(yàn)證過程.并在計(jì)算量和保守性兩方面將兩種方法進(jìn)行了詳細(xì)的分析對(duì)比.分析結(jié)果表明:用簡(jiǎn)化后的算法計(jì)算商遷移系統(tǒng)的遷移關(guān)系,在保持計(jì)算效果的基礎(chǔ)上,不但減少了系統(tǒng)過近似的保守性,而且僅需要少量的流管道計(jì)算,就能求出系統(tǒng)的遷移關(guān)系. 最后,在對(duì)全文的研究工作進(jìn)行了總結(jié)的基礎(chǔ)上,對(duì)今