本文關(guān)鍵詞：基于協(xié)同驗證與混成關(guān)系的混成系統(tǒng)形式化分析驗證　出處：《華東師范大學》2016年博士論文　論文類型：學位論文

  更多相關(guān)文章： 混成系統(tǒng) 形式化方法 仿真 驗證 霍爾邏輯 混成關(guān)系 可滿足性模理論

【摘要】：隨著軟件、集成電路、網(wǎng)絡及通信技術(shù)的飛速發(fā)展,人類生存的自然物理世界與計算機科學領域之間的聯(lián)系和相互影響愈加的緊密和重要�；斐上到y(tǒng),作為一個融合并體現(xiàn)自然物理世界的連續(xù)特性及計算的離散特性的基本模型,在最近三十年間,一直受到來自數(shù)學、控制、計算機甚至生物化學等眾多學科無數(shù)專家學者的研究和關(guān)注。目前,形式化方法在混成系統(tǒng)的眾多研究理論和方法中占有重要的一席。本文,我們主要研究混成系統(tǒng)的建模、仿真和形式化驗證�，F(xiàn)有的形式化驗證技術(shù)無法克服狀態(tài)空間爆炸問題,當混成系統(tǒng)的規(guī)模較大時,驗證工具往往無法給出驗證結(jié)果,從而無法判定模型的正確性和安全性,這使得混成系統(tǒng)的形式化驗證理論和方法對工業(yè)界的影響相當有限。為了融合現(xiàn)有的仿真和驗證技術(shù),我們提出協(xié)同驗證方法,使仿真與驗證的方法和技術(shù)相結(jié)合,充分發(fā)揮仿真技術(shù)在大規(guī)模復雜系統(tǒng)分析上的優(yōu)勢,基于仿真結(jié)果的反饋,對驗證模型進行抽象,同時利用驗證技術(shù)在模型檢驗方面的優(yōu)勢保障模型的正確性和安全性。另一方面,基于驗證結(jié)果的反饋,可實現(xiàn)仿真模型的優(yōu)化和更有效的仿真。如此,通過驗證與仿真的相互反饋,逐步實現(xiàn)高效、可信的混成系統(tǒng)設計與開發(fā)。此外,混成系統(tǒng)建模語言對于實現(xiàn)形式化方法在工業(yè)界的廣泛應用也是極其重要的。一個結(jié)構(gòu)良好、使用方便的建模語言往往更易于被工業(yè)界的設計和開發(fā)人員所接受,從而得以推廣和應用。華東師范大學何積豐院士最新提出的混成系統(tǒng)建模語言(在本文中,我們使用HML (Hybrid Modeling Language)表示該建模語言),在語法結(jié)構(gòu)上具有設計良好、語法簡單等特性。此外,該建模語言還具有很強的可擴展性,非常適合系統(tǒng)設計和開發(fā)人員在實際工作中使用。為了支持HML語言的形式化驗證,我們基于混成關(guān)系理論給出相應的霍爾邏輯推理規(guī)則,并將HML模型轉(zhuǎn)換為SMT (Satisfiability Modulo Theories)公式進行約束求解,以實現(xiàn)混成系統(tǒng)的仿真和自動化驗證。下面,我們從三個方面對本論文的主要貢獻進行總結(jié)：·方法貢獻基于對混成系統(tǒng)仿真和驗證技術(shù)的優(yōu)勢及劣勢分析,我們提出反饋演進的混成系統(tǒng)模型設計和分析方法。通過仿真技術(shù),我們可以實現(xiàn)大規(guī)模復雜系統(tǒng)的分析,但是仿真無法完全覆蓋系統(tǒng)所有可能的狀態(tài)和執(zhí)行路徑,所以基于仿真的系統(tǒng)設計和開發(fā)方法,容易產(chǎn)生遺漏和失誤,從而為工業(yè)生產(chǎn)和公共安全帶來嚴重的安全隱患�；谛问交炞C,我們可以對系統(tǒng)所有可能的狀態(tài)進行分析和檢查,從而能夠保證系統(tǒng)的正確性和安全性。不過,形式化驗證不能有效地對大規(guī)模復雜系統(tǒng)進行分析。因此,整合仿真與驗證來對混成系統(tǒng)進行分析是很有必要的。我們提出的反饋演進方法充分利用仿真與驗證各自的優(yōu)勢,使二者的分析驗證能力得以互補,通過分析驗證結(jié)果互反饋的方式逐步實現(xiàn)大規(guī)模復雜混成系統(tǒng)的可信設計與開發(fā)�！だ碚撠暙I混成關(guān)系理論將混成系統(tǒng)的行為表示為三種系統(tǒng)執(zhí)行狀態(tài)下的條件約束,基于離散和連續(xù)動態(tài)行為的特性,分別對動態(tài)行為執(zhí)行前、執(zhí)行過程中以及執(zhí)行結(jié)束時所滿足的條件進行約定。受混成關(guān)系基本思想的啟發(fā),我們將混成關(guān)系與霍爾邏輯相結(jié)合,給出一種新的霍爾邏輯推理規(guī)則,以支持混成系統(tǒng)建模語言HML的推理驗證。與以往的推理系統(tǒng)不同的是,在微分方程的處理上,我們的推理規(guī)則并不依賴于特定的方程或不變式求解技術(shù)。在我們的推理系統(tǒng)中,推理規(guī)則實現(xiàn)的是一個驗證的框架,當我們需要對具體的微分方程進行處理時可以自由地選擇數(shù)學領域成熟的技術(shù)來分析。邏輯規(guī)則與數(shù)學求解的分離可以極大地簡化推理規(guī)則的復雜度,并支持規(guī)則的可擴展性,使我們更好地專注于模型結(jié)構(gòu)和系統(tǒng)行為驗證過程的邏輯部分�！嵺`貢獻本文包含豐富的混成系統(tǒng)案例分析,如：地鐵屏蔽門控制、列車防碰撞控制、水箱水位控制、倒立擺控制等等。這些案例分析是對我們提出的理論和方法的檢驗,能夠體現(xiàn)所提出的理論和方法的可行性與有效性。此外,我們還基于混成關(guān)系理論的基本思想,提出將基于HML語言建立的混成系統(tǒng)模型轉(zhuǎn)換為SMT公式的方法,并整合SMT求解器dReal的約束求解技術(shù),開發(fā)了相應的原型工具,實現(xiàn)了HML模型仿真和驗證的自動化。該工作在混成系統(tǒng)開發(fā)和驗證方面為我們的下一步研究打下了堅實的基礎。
【學位授予單位】：華東師范大學
【學位級別】：博士
【學位授予年份】：2016
【分類號】：TP311.52
，

本文編號：1312773