基于CPS的實時系統(tǒng)的面向方面的形式化驗證方法.pdf

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

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

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

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