面向CPS時(shí)空性質(zhì)的混成AADL建模與模型轉(zhuǎn)換方法，以解決CPS缺乏時(shí)間與空間統(tǒng)一建模與驗(yàn)證方法的問(wèn)題。首先，擴(kuò)展AADL行為附件的時(shí)空描述能力，提出混成AADL，用于建模CPS的時(shí)空性質(zhì)；其次，在進(jìn)程代數(shù)中引入微分方程以及位置描述提出HP?TCSP，能夠驗(yàn)證CPS的時(shí)空性質(zhì)；再次，通過(guò)模型轉(zhuǎn)換將混成AADL轉(zhuǎn)換為HP?TCSP，從而可以將混成AADL描述的CPS模型在HP?TCSP中進(jìn)行時(shí)空一致性驗(yàn)證。

技術(shù)領(lǐng)域

本發(fā)明涉及建模與模型轉(zhuǎn)換方法，具體涉及一種面向CPS時(shí)空性質(zhì)的混成AADL建模與模型轉(zhuǎn)換方法。

背景技術(shù)

近年來(lái),隨著云計(jì)算、物聯(lián)網(wǎng)與5G技術(shù)的快速發(fā)展，CPS的應(yīng)用已經(jīng)覆蓋到我們生產(chǎn)生活的各個(gè)方面，其安全性問(wèn)題也受到了廣泛關(guān)注，尤其在很多安全系數(shù)較高的CPS場(chǎng)景中，如航空航天、交通運(yùn)輸、醫(yī)療衛(wèi)生等系統(tǒng)，系統(tǒng)的安全性驗(yàn)證[1]顯得尤為重要。與傳統(tǒng)的嵌入式系統(tǒng)不同，CPS更加注重計(jì)算過(guò)程與物理過(guò)程的實(shí)時(shí)有效交互以及系統(tǒng)位置的變化對(duì)系統(tǒng)參數(shù)的影響[2]。因此，如何驗(yàn)證在復(fù)雜的運(yùn)行環(huán)境下CPS的時(shí)空一致性以保障CPS的安全性是當(dāng)前面臨的挑戰(zhàn)。

體系結(jié)構(gòu)分析與設(shè)計(jì)語(yǔ)言AADL是于2004年由自動(dòng)化工程師學(xué)會(huì)發(fā)布的建模語(yǔ)言[3]，AADL自提出以來(lái)受廣泛關(guān)注。該語(yǔ)言基于系統(tǒng)構(gòu)件層次化的結(jié)構(gòu)設(shè)計(jì)方法，能夠以統(tǒng)一的方式對(duì)硬件與軟件進(jìn)行抽象建模，支持高度可演化系統(tǒng)的開發(fā)，AADL語(yǔ)言能提供所需構(gòu)件之間的分層功能，同時(shí)支持文本和圖形化的描述方式從而快速建模，其行為附件支持對(duì)性質(zhì)的擴(kuò)展，在CPS建模過(guò)程中具有很高的靈活性和實(shí)用性，因此AADL目前已經(jīng)成為許多學(xué)者對(duì)CPS建模的首選語(yǔ)言且在CPS領(lǐng)域廣泛使用。文獻(xiàn)[4]基于AADL對(duì)云信息物理融合系統(tǒng)建模并進(jìn)行數(shù)據(jù)質(zhì)量分析、實(shí)時(shí)性能分析和資源消耗分析。文獻(xiàn)[5]將模型檢查集成到設(shè)計(jì)過(guò)程中,根據(jù)AADL中的高級(jí)規(guī)范生成定時(shí)自動(dòng)機(jī)模型,從而將模型檢查技術(shù)集成到CPS設(shè)計(jì)過(guò)程中。然而AADL并沒(méi)有足夠的能力描述CPS的性質(zhì)以及異構(gòu)特性與連續(xù)行為等特點(diǎn)，因此，相關(guān)學(xué)者在AADL語(yǔ)言上進(jìn)行相應(yīng)的擴(kuò)展從而更好的對(duì)CPS進(jìn)行研究。Jing Liu[6]等人針對(duì)CPS的連續(xù)行為以及網(wǎng)絡(luò)組件和物理組件之間的交互進(jìn)行建模提出構(gòu)造新的AADL子語(yǔ)言AADL+的方法。Renya He[7]等人提出基于擴(kuò)展AADL的CPS集成建模框架描述方法，實(shí)現(xiàn)計(jì)算實(shí)體、物理實(shí)體和交互實(shí)體的統(tǒng)一描述。Haolan Zhan[8]等人將AADL與Simulink/Stateflow結(jié)合，提供統(tǒng)一的圖形化協(xié)同建模形式，從軟件、硬件和物理三個(gè)角度統(tǒng)一支持CPS的設(shè)計(jì)。此外，AADL本身還是一種半形式化的建模語(yǔ)言，無(wú)法保證所建立的CPS模型的安全性，因此有必要對(duì)使用AADL建模的模型進(jìn)行安全性驗(yàn)證。

通信順序進(jìn)程CSP(Communicating Sequential Process)是Hoare[9]在1978年建立的一種適合于分布式并發(fā)軟件規(guī)格和設(shè)計(jì)的形式化方法。1986年，牛津的Reed和Roscoe對(duì)CSP進(jìn)行實(shí)時(shí)擴(kuò)展,提出了時(shí)間通信順序進(jìn)程TCSP(Timed Communicating SequentialProcess)[10]。進(jìn)程代數(shù)是一種解決并發(fā)系統(tǒng)通信問(wèn)題的形式化方法，能夠描述CPS中的事件的并發(fā)、同步、異步等問(wèn)題。但是TCSP是離散模型，且只有時(shí)間性質(zhì)的描述能力，因此有必要對(duì)TCSP進(jìn)行空間描述能力與連續(xù)行為能力的擴(kuò)展，擴(kuò)展后的TCSP能夠?qū)PS的時(shí)空一致性進(jìn)行驗(yàn)證。