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