基于Modelica-AADL的信息物理系統(tǒng)形式化建模與性能評價
發(fā)布時間:2021-11-09 16:38
信息物理融合系統(tǒng)(CPS)是物聯(lián)網(wǎng)進一步發(fā)展的產(chǎn)物,CPS將物理過程與信息計算過程緊密聯(lián)系,是一種復(fù)雜的混合系統(tǒng),Modelica與AADL是適合用以信息物理融合系統(tǒng)的嵌入式系統(tǒng)體系結(jié)構(gòu)建模語言,本文基于Modelica-AADL的建模方式,制定了適用于CPS的形式化性能評價語言及算法,完成系統(tǒng)的性能需求的規(guī)約,進一步分析與評價信息物理融合系統(tǒng)的相關(guān)性能。首先,應(yīng)用兩種不相關(guān)的建模語言Modelica與AADL為CPS建模,構(gòu)建一種組合式建模方式Modelica-AADL,其中,Modelica應(yīng)用于物理系統(tǒng)的建模,AADL應(yīng)用于信息系統(tǒng)的建模,并對Modelica進行了相關(guān)的概率擴展,設(shè)計了接口將兩種建模方式組合。同時,將Z語言引入到Modelica-AADL模型中,用以描述系統(tǒng)中的數(shù)據(jù)約束。為了進行系統(tǒng)分析評價工作,制定了相關(guān)規(guī)則與算法將非形式化的Modelica-AADL描述轉(zhuǎn)換成形式化的概率混成自動機模型。之后定義面向CPS的形式化性能評價語言CTEL,結(jié)合相關(guān)具有統(tǒng)計意義的評價量計算方式,計算出性能評價的值,利用CTEL對系統(tǒng)的性能性質(zhì)進行描述,得到分析結(jié)果。最后,結(jié)合統(tǒng)計方...
【文章來源】:南京航空航天大學(xué)江蘇省 211工程院校
【文章頁數(shù)】:85 頁
【學(xué)位級別】:碩士
【部分圖文】:
智慧城市架構(gòu)案例CPS在生活中應(yīng)用場景越來越廣,人們對于相應(yīng)系統(tǒng)的質(zhì)量需求快速提升
圖 1.3 CPS 的結(jié)構(gòu)實例CPS 軟件的形式化建模是CPS軟件屬性驗證的前提和基礎(chǔ)。關(guān)于CPS軟件的形式化可以歸納分為如下幾類:形式化推理方法推理證明需要數(shù)學(xué)邏輯描述系統(tǒng)方面的特征,邏輯形式由公理和推論組成的規(guī)則定理證明器的支撐。常用的檢驗證明器包括 HOL、Coq、LCF 和 LEGO[5];復(fù)合證 PVS[6]、Analytica(將符號代數(shù)與定理證明整合)和 Step(將決策過程與交互式推合),用戶推演推算工具包括 RRL、LP、ACL2、Eves 等[7]。Petri 網(wǎng)建模Petri 網(wǎng)是應(yīng)用廣泛的計算機領(lǐng)域傳統(tǒng)的模型分析及驗證方法,適用于描述系統(tǒng)中步行為。通常,為了增強能力,將擴展信息引入Petri 網(wǎng),不會破壞Petri 網(wǎng)結(jié)構(gòu)的步和并發(fā)的表達(dá)。基于Petri 網(wǎng)的驗證工具目前比較通用的是EXSPECT。自動機建模
圖 3.1 簡單電路舉例p)表示電流從電源 VS 進入電阻 R,系統(tǒng)狀態(tài)由表示電流從電阻 R 流到電容 C,系統(tǒng)狀態(tài)由1s)表示電流從電容 C 流到電源 VS 的另一極,系統(tǒng)可以表示為1 230 1 2 3c ccs s s s,其中是變量 v,i 和一些常量 c,r 等的具體值狀態(tài) 中引入概率因子物理事件進行響應(yīng),而現(xiàn)實中的物理事件常常很有必要。性有助于我們將概率因子引入其中。Modelic者事件的發(fā)生?梢阅M事件的瞬時發(fā)生,改為。理事件行為產(chǎn)生的系統(tǒng)響應(yīng)建立 Modelica 對 CPS 中通常需要傳感器來監(jiān)測物理環(huán)境中的
【參考文獻】:
期刊論文
[1]信息物理融合系統(tǒng)概述[J]. 姜宏. 電腦知識與技術(shù). 2011(35)
[2]信息物理融合系統(tǒng)研究綜述[J]. 王中杰,謝璐璐. 自動化學(xué)報. 2011(10)
[3]信息物理融合系統(tǒng)(CPS)研究綜述[J]. 黎作鵬,張?zhí)祚Y,張菁. 計算機科學(xué). 2011(09)
[4]基于時間自動機的物聯(lián)網(wǎng)服務(wù)建模和驗證[J]. 李力行,金芝,李戈. 計算機學(xué)報. 2011(08)
[5]復(fù)雜嵌入式實時系統(tǒng)體系結(jié)構(gòu)設(shè)計與分析語言:AADL[J]. 楊志斌,皮磊,胡凱,顧宗華,馬殿富. 軟件學(xué)報. 2010(05)
本文編號:3485707
【文章來源】:南京航空航天大學(xué)江蘇省 211工程院校
【文章頁數(shù)】:85 頁
【學(xué)位級別】:碩士
【部分圖文】:
智慧城市架構(gòu)案例CPS在生活中應(yīng)用場景越來越廣,人們對于相應(yīng)系統(tǒng)的質(zhì)量需求快速提升
圖 1.3 CPS 的結(jié)構(gòu)實例CPS 軟件的形式化建模是CPS軟件屬性驗證的前提和基礎(chǔ)。關(guān)于CPS軟件的形式化可以歸納分為如下幾類:形式化推理方法推理證明需要數(shù)學(xué)邏輯描述系統(tǒng)方面的特征,邏輯形式由公理和推論組成的規(guī)則定理證明器的支撐。常用的檢驗證明器包括 HOL、Coq、LCF 和 LEGO[5];復(fù)合證 PVS[6]、Analytica(將符號代數(shù)與定理證明整合)和 Step(將決策過程與交互式推合),用戶推演推算工具包括 RRL、LP、ACL2、Eves 等[7]。Petri 網(wǎng)建模Petri 網(wǎng)是應(yīng)用廣泛的計算機領(lǐng)域傳統(tǒng)的模型分析及驗證方法,適用于描述系統(tǒng)中步行為。通常,為了增強能力,將擴展信息引入Petri 網(wǎng),不會破壞Petri 網(wǎng)結(jié)構(gòu)的步和并發(fā)的表達(dá)。基于Petri 網(wǎng)的驗證工具目前比較通用的是EXSPECT。自動機建模
圖 3.1 簡單電路舉例p)表示電流從電源 VS 進入電阻 R,系統(tǒng)狀態(tài)由表示電流從電阻 R 流到電容 C,系統(tǒng)狀態(tài)由1s)表示電流從電容 C 流到電源 VS 的另一極,系統(tǒng)可以表示為1 230 1 2 3c ccs s s s,其中是變量 v,i 和一些常量 c,r 等的具體值狀態(tài) 中引入概率因子物理事件進行響應(yīng),而現(xiàn)實中的物理事件常常很有必要。性有助于我們將概率因子引入其中。Modelic者事件的發(fā)生?梢阅M事件的瞬時發(fā)生,改為。理事件行為產(chǎn)生的系統(tǒng)響應(yīng)建立 Modelica 對 CPS 中通常需要傳感器來監(jiān)測物理環(huán)境中的
【參考文獻】:
期刊論文
[1]信息物理融合系統(tǒng)概述[J]. 姜宏. 電腦知識與技術(shù). 2011(35)
[2]信息物理融合系統(tǒng)研究綜述[J]. 王中杰,謝璐璐. 自動化學(xué)報. 2011(10)
[3]信息物理融合系統(tǒng)(CPS)研究綜述[J]. 黎作鵬,張?zhí)祚Y,張菁. 計算機科學(xué). 2011(09)
[4]基于時間自動機的物聯(lián)網(wǎng)服務(wù)建模和驗證[J]. 李力行,金芝,李戈. 計算機學(xué)報. 2011(08)
[5]復(fù)雜嵌入式實時系統(tǒng)體系結(jié)構(gòu)設(shè)計與分析語言:AADL[J]. 楊志斌,皮磊,胡凱,顧宗華,馬殿富. 軟件學(xué)報. 2010(05)
本文編號:3485707
本文鏈接:http://www.sikaile.net/kejilunwen/wltx/3485707.html
最近更新
教材專著