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

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

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

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

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