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

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

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

【學位級別】：碩士

【部分圖文】：

CheckMate模塊

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

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


本文編號：3015607