基于CPS的實時系統的面向方面的形式化驗證方法.pdf

1、Cyber-physical網絡環(huán)境下的實時系統是一個綜合計算、網絡和物理環(huán)境的多維復雜系統,通過3C(Computation、Conmunication、Control)技術的有機融合與深度協作,實現大型工程系統的實時感知、動態(tài)控制和信息服務。Cyber-physical網絡環(huán)境下的實時系統實現計算、通信與物理系統的一體化設計,可使系統更加可靠、高效、實時協同,具有重要而廣泛的應用前景。近年來,Cyber—physical網絡環(huán)境下的

2、實時系統不僅已成為國內外學術界和科技界研究開發(fā)的重要方向,預計也將成為企業(yè)界優(yōu)先發(fā)展的產業(yè)領域。開展Cyber-physical網絡環(huán)境下的實時系統研究與應用對于加快我國培育推進工業(yè)化與信息化融合具有重要意義。
　　 本文試圖建立一種面向方面的實時系統形式化驗證方法,這種方法對形式化驗證方法的進行了面向方面的擴展。以分布式實時軟件非功能特性的面向方面的形式化模型為基礎,研究Cyber-physical網絡環(huán)境下的實時系統非功能特

3、性的面向方面驗證理論、方法和關鍵技術,利用面向方面的技術解決由Cyber-physical網絡環(huán)境下的實時系統非功能特性的帶來的驗證問題的復雜性控制,使得Cyber-physical網絡環(huán)境下的實時系統非功能特性的能在自動化程度和系統規(guī)模上適應系統的需要。Cyber-physical網絡環(huán)境下的實時系統非功能特性的的多種特性使得驗證的復雜性呈指數爆炸,在形式驗證中可以采用面向方面的技術進行有效的抽象和分解。
　　 由于CPS和待

4、檢驗的性質可分別表示成一個邏輯公式,要想檢驗系統是否滿足該性質,只需在邏輯系統中檢驗此二公式是否有蘊含關系；同樣,要想檢驗系統和一個方面模塊之間是否具有蘊含關系,只需驗證方面模塊和系統相應的邏輯公式是否具有蘊含關系。在第三章中我們將看到,一種面向方面的VDM++方法對于建立系統模型非常有效。在第四章中我們將看到一個應用的例子——空中交通管制的語音通信系統,并應用基于面向方面的VDM++對系統進行驗證。
　　 本文的工作重點就是要