混雜系統(tǒng)的形式驗(yàn)證技術(shù)是利用數(shù)學(xué)分析方法對(duì)混雜系統(tǒng)的安全性進(jìn)行驗(yàn)證。近十年來,模型驗(yàn)證技術(shù)是形式驗(yàn)證研究的主要方法。模型驗(yàn)證技術(shù)是指,利用計(jì)算機(jī)強(qiáng)大的計(jì)算功能自動(dòng)地對(duì)混雜系統(tǒng)的數(shù)學(xué)模型進(jìn)行整個(gè)狀態(tài)空間中進(jìn)行遍歷搜索,對(duì)系統(tǒng)所有可能的運(yùn)行軌跡進(jìn)行收斂計(jì)算或過近似計(jì)算,以檢驗(yàn)系統(tǒng)的實(shí)現(xiàn)方案是否滿足系統(tǒng)的設(shè)計(jì)要求。論文首先介紹了模型驗(yàn)證的概念和特點(diǎn),常用的混雜系統(tǒng)建模方法如混雜自動(dòng)機(jī)、混雜Petri網(wǎng)、層次結(jié)構(gòu)和時(shí)段演算。分析了可達(dá)集的兩種計(jì)算方法—前向和后向可達(dá)集算法,對(duì)可達(dá)集的過近似方法作了系統(tǒng)的闡述。最后詳細(xì)介紹了模型驗(yàn)證的國內(nèi)外研究狀況和常用的模型驗(yàn)證工具。針對(duì)混雜系統(tǒng)連續(xù)子系統(tǒng)和離散子系統(tǒng)相互作用的特點(diǎn),研究了混雜自動(dòng)機(jī)模、多面體混雜自動(dòng)機(jī)和混雜I/O自動(dòng)機(jī)的建模方法;對(duì)于混雜系統(tǒng)的流管道過近似問題,給出了齊諾多面體（zonotopes）的基于中心點(diǎn)和生成元（generators）的表達(dá)式和過近似算法,分析了該算法的保守性、封閉性、集合交并處理能力以及收斂性。通過比較凸多面體過近似和齊諾多面體過近似算法的適用對(duì)象、計(jì)算方法、過近似保守性和隨維數(shù)增長的計(jì)算復(fù)雜度,對(duì)兩種算法的優(yōu)劣和特... 

【文章來源】：合肥工業(yè)大學(xué)安徽省 211工程院校 教育部直屬院校

【文章頁數(shù)】：80 頁

【學(xué)位級(jí)別】：碩士

【部分圖文】：

CheckMate模塊

域的詳細(xì)說明，請(qǐng)參見參數(shù)輸入部分。連續(xù)系統(tǒng)切換模塊和該模塊的參數(shù)如圖3.2所示：圖3.2 切換連續(xù)系統(tǒng)模塊和參數(shù)對(duì)話框3.2 多面體閾值事件模塊（Polyhedral Threshold Block，PTHB）圖 3.3 多面體閾值模塊和參數(shù)對(duì)話框

多面體閾值模塊和參數(shù)對(duì)話框


本文編號(hào)：3015607