混合系統(tǒng)的形式驗證方法及其應(yīng)用.pdf

1、在混合系統(tǒng)中，離散事件和連續(xù)動態(tài)行為相互作用的特性使得系統(tǒng)開發(fā)的正確性難以保證，尤其對于安全悠關(guān)的系統(tǒng)，如電力系統(tǒng)和化工系統(tǒng)，錯誤運行將造成重大損失。而形式驗證的目的在于檢驗混合系統(tǒng)是否在任何環(huán)境下都能安全運行?；旌舷到y(tǒng)的形式驗證是混合系統(tǒng)研究的一個熱點和難點，至今仍未出現(xiàn)比較成熟的方法體系，驗證工具大部分停留在實驗室研究階段，距離能夠廣泛適用于工業(yè)界的目標仍有相當遠的距離。 本文所有論述均圍繞著解決混合系統(tǒng)的形式驗證問題這個主

2、題展開，主要工作有： 1.在國內(nèi)混合系統(tǒng)的形式驗證研究剛剛起步的情況下，通過大量的國內(nèi)外文獻閱讀，對各種基于模型檢驗的混合系統(tǒng)形式驗證方法進行了整理和總結(jié)，歸納出基于模型檢驗的混合系統(tǒng)形式驗證原理，包括可達集的計算、商遷移系統(tǒng)、仿真對和混合系統(tǒng)形式驗證的過程，并對目前主要的驗證工具進行了分析和比較。 2.研究了基于流管道和切換面劃分的混合系統(tǒng)形式驗證方法：在研究多面體不變集混合自動機和離散抽象遷移系統(tǒng)概念的基礎(chǔ)上，分析了

3、有限狀態(tài)近似商遷移系統(tǒng)的計算方法，包括閾值切換面劃分、遷移系統(tǒng)狀態(tài)的確定、流管道計算和遷移關(guān)系的確定。 3.當系統(tǒng)為線性定常連續(xù)動態(tài)并且初始區(qū)域為凸集時，針對連續(xù)動態(tài)流管道計算的困難，提出有關(guān)系統(tǒng)演化軌跡規(guī)律的具體結(jié)論并加以證明，依據(jù)這些結(jié)論對商遷移系統(tǒng)中遷移關(guān)系的計算方法進行了改進，改進的遷移關(guān)系計算將節(jié)省大量的計算時間和計算量。 4.根據(jù)一個倒立擺實例及其控制規(guī)范要求，給出了適用于驗證工具CheckMate的系統(tǒng)描述