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

1、混合系統(tǒng)是連續(xù)變量過程和離散事件過程并存,且相互交換信息的一類動態(tài)系統(tǒng).八十年代后期,隨著微型計算機(jī)、大型通訊網(wǎng)和微處理器在控制領(lǐng)域的大量應(yīng)用,一批反映先進(jìn)技術(shù)發(fā)展方向的人造系統(tǒng)大量涌現(xiàn),連續(xù)動態(tài)過程與離散事件混合的系統(tǒng)廣泛出現(xiàn)于生產(chǎn)實(shí)際中,混合系統(tǒng)成為自動控制和計算機(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)證的異同,對現(xiàn)有的基于模型檢驗(yàn)的混合系統(tǒng)形式化驗(yàn)證工具進(jìn)行了對比與分析. 針對混合系統(tǒng)既包含連續(xù)動態(tài)過程又包含離散事件過程的特點(diǎn),研究了通過混合自動機(jī)模型進(jìn)行混合系統(tǒng)建模的方法;對于混合系統(tǒng)驗(yàn)證中的模型檢驗(yàn)問題,分析了計算樹邏輯CTL和基于動作的時序邏輯ACTL. 對可達(dá)集的表示和計算方法進(jìn)行了較為深入的研究:對比了使用凸多面體、超矩形和有向矩形殼表示可達(dá)集時,在過近似的保守性,計算的復(fù)雜度,集合交、并處理能力和維

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

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