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

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

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

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

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