本文關(guān)鍵詞：面向服務(wù)的信息物理融合系統(tǒng)建模與驗(yàn)證

  更多相關(guān)文章： 信息物理融合系統(tǒng) 面向服務(wù) 模型驗(yàn)證 時(shí)間自動(dòng)機(jī) Uppaal

【摘要】：針對(duì)信息物理融合系統(tǒng)(CPS)中建模與驗(yàn)證面臨的問(wèn)題與挑戰(zhàn),基于服務(wù)組合的思想,提出一種CPS建模與驗(yàn)證方法。首先,綜合分析已有研究成果,提出一種CPS的組成結(jié)構(gòu),包含物理世界、感知系統(tǒng)、信息處理系統(tǒng)、控制系統(tǒng)及時(shí)間約束。基于該結(jié)構(gòu)提出CPS資源的服務(wù)分類及組成框架,并利用時(shí)間自動(dòng)機(jī)理論,提出CPS物理環(huán)境建模方法、CPS原子服務(wù)建模方法及服務(wù)組合方法。最后,通過(guò)案例設(shè)計(jì)和模型檢測(cè)工具Uppaal,分別對(duì)系統(tǒng)安全性、可達(dá)性、活性及時(shí)間約束四種類型的性質(zhì)進(jìn)行了相關(guān)驗(yàn)證。結(jié)果表明,系統(tǒng)通過(guò)了這些性質(zhì)的驗(yàn)證,這也證明了面向服務(wù)的CPS建模方法的正確性。
【作者單位】： 國(guó)防科學(xué)技術(shù)大學(xué)信息系統(tǒng)工程重點(diǎn)實(shí)驗(yàn)室;
【關(guān)鍵詞】： 信息物理融合系統(tǒng) 面向服務(wù) 模型驗(yàn)證 時(shí)間自動(dòng)機(jī) Uppaal
【基金】：國(guó)家863計(jì)劃項(xiàng)目(2011AA010106)
【分類號(hào)】：TP393.09
【正文快照】： 0引言2006年,美國(guó)國(guó)家科學(xué)基金會(huì)(National ScienceFoundation,NSF)提出了信息物理融合系統(tǒng)(Cyber PhysicalSystem,CPS)的概念[1]。它指出,CPS是一個(gè)綜合計(jì)算、網(wǎng)絡(luò)和物理環(huán)境的分布式、實(shí)時(shí)性系統(tǒng),通過(guò)計(jì)算、通信與控制的有機(jī)融合和深度協(xié)作,實(shí)現(xiàn)工程系統(tǒng)的實(shí)時(shí)感知、動(dòng)態(tài)控

【參考文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前4條

1 譚朋柳;舒堅(jiān);吳振華;;一種信息-物理融合系統(tǒng)體系結(jié)構(gòu)[J];計(jì)算機(jī)研究與發(fā)展;2010年S2期

2 陳麗娜;王小樂;鄧蘇;;CPS體系結(jié)構(gòu)設(shè)計(jì)[J];計(jì)算機(jī)科學(xué);2011年05期

3 李力行;金芝;李戈;;基于時(shí)間自動(dòng)機(jī)的物聯(lián)網(wǎng)服務(wù)建模和驗(yàn)證[J];計(jì)算機(jī)學(xué)報(bào);2011年08期

4 王小樂;陳麗娜;黃宏斌;鄧蘇;;一種面向服務(wù)的CPS體系框架[J];計(jì)算機(jī)研究與發(fā)展;2010年S2期

【共引文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前10條

1 龔鑓;李蘇劍;;基于CPS理論的城市交通控制與誘導(dǎo)融合框架[J];公路交通科技;2012年05期

2 汪治華;張亞杰;杜凱;;交通CPS體系結(jié)構(gòu)設(shè)計(jì)[J];公路交通科技;2012年S1期

3 高治軍;王洪玉;王鑫;韓忠華;;智能建筑室內(nèi)環(huán)境分布式可計(jì)算WSN任務(wù)調(diào)度研究[J];傳感技術(shù)學(xué)報(bào);2014年03期

4 王樂達(dá);;倉(cāng)庫(kù)管理信息物理融合系統(tǒng)[J];計(jì)算機(jī)光盤軟件與應(yīng)用;2014年03期

5 孫圣力;鄭志高;王平;劉京;;RTDP系統(tǒng)網(wǎng)絡(luò)體系結(jié)構(gòu)及其關(guān)鍵技術(shù)[J];北京郵電大學(xué)學(xué)報(bào);2014年S1期

6 王小樂;黃宏斌;鄧蘇;陳麗娜;;信息物理系統(tǒng)資源能力建模[J];計(jì)算機(jī)科學(xué);2012年02期

7 陳志輝;;基于時(shí)間自動(dòng)機(jī)的信息物理融合系統(tǒng)建模與驗(yàn)證[J];計(jì)算機(jī)與現(xiàn)代化;2012年10期

8 周宇;胡軍;葛季棟;;一種層次式時(shí)間自動(dòng)機(jī)模型檢測(cè)方法[J];計(jì)算機(jī)應(yīng)用與軟件;2012年11期

9 陳海明;崔莉;謝開斌;;物聯(lián)網(wǎng)體系結(jié)構(gòu)與實(shí)現(xiàn)方法的比較研究[J];計(jì)算機(jī)學(xué)報(bào);2013年01期

10 封飛;陳名才;張廣泉;邵玉珍;李燁靜;;基于混成自動(dòng)機(jī)的車聯(lián)網(wǎng)服務(wù)建模方法[J];南通大學(xué)學(xué)報(bào)(自然科學(xué)版);2013年02期

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前8條

1 劉志明;對(duì)等存儲(chǔ)系統(tǒng)數(shù)據(jù)管理研究[D];國(guó)防科學(xué)技術(shù)大學(xué);2011年

2 李永福;面向T-CPS的微觀交通認(rèn)知方法及相關(guān)研究[D];重慶大學(xué);2012年

3 劉洪濤;高性能傳感器網(wǎng)絡(luò)體系結(jié)構(gòu)及可用帶寬估計(jì)研究[D];廣東工業(yè)大學(xué);2012年

4 董新平;物聯(lián)網(wǎng)產(chǎn)業(yè)成長(zhǎng)研究[D];華中師范大學(xué);2012年

5 倫永亮;信息物理融合系統(tǒng)優(yōu)化調(diào)度理論與方法的研究[D];廣東工業(yè)大學(xué);2012年

6 張洪昌;信息物理融合的機(jī)電產(chǎn)品數(shù)字化設(shè)計(jì)關(guān)鍵技術(shù)研究[D];華中科技大學(xué);2012年

7 任慰;以實(shí)時(shí)操作系統(tǒng)為中心的嵌入式系統(tǒng)平臺(tái)化設(shè)計(jì)研究[D];華中科技大學(xué);2013年

8 俞磊;基于物聯(lián)網(wǎng)技術(shù)的智慧醫(yī)院架構(gòu)及服務(wù)訪問(wèn)研究[D];合肥工業(yè)大學(xué);2014年

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前10條

1 韋佳;基于ZigBee無(wú)線傳感器網(wǎng)絡(luò)的智能開關(guān)研究與設(shè)計(jì)[D];江南大學(xué);2012年

2 吳帥;實(shí)時(shí)信息物理系統(tǒng)的中間件的研究[D];廣東工業(yè)大學(xué);2012年

3 柳求金;基于形式化的信息物理系統(tǒng)的建模與驗(yàn)證[D];廣東工業(yè)大學(xué);2012年

4 蔡熱文;基于面向方面的時(shí)間Petri網(wǎng)的實(shí)時(shí)信息物理系統(tǒng)的建模[D];廣東工業(yè)大學(xué);2012年

5 仲昌平;基于多元邏輯回歸的CPS鏈路質(zhì)量保障算法研究[D];西南交通大學(xué);2012年

6 李云霄;鐵路信息物理融合系統(tǒng)的分析與設(shè)計(jì)方法[D];廣東工業(yè)大學(xué);2013年

7 雷瑤;信息物理融合系統(tǒng)的形式化建模與分析[D];廣東工業(yè)大學(xué);2013年

8 魯川;面向信息物理融合系統(tǒng)的實(shí)時(shí)時(shí)空調(diào)度算法[D];廣東工業(yè)大學(xué);2013年

9 易良辰;普適環(huán)境下基于抽象狀態(tài)機(jī)的服務(wù)組合的分析與驗(yàn)證[D];上海交通大學(xué);2013年

10 黎曉波;網(wǎng)絡(luò)拓?fù)淇焖僮兓腁d-Hoc路由協(xié)議研究[D];北京郵電大學(xué);2013年

【二級(jí)參考文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前2條

1 侯麗珊;金芝;吳步丹;;需求驅(qū)動(dòng)的Web服務(wù)建模及其驗(yàn)證:一個(gè)基于本體的方法[J];中國(guó)科學(xué)E輯:信息科學(xué);2006年10期

2 徐志偉;李沛旭;查禮;;計(jì)算機(jī)系統(tǒng)變革性研究的4個(gè)問(wèn)題[J];計(jì)算機(jī)研究與發(fā)展;2008年12期

【相似文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前10條

1 高冠龍;周清雷;;時(shí)間自動(dòng)機(jī)與網(wǎng)絡(luò)協(xié)議驗(yàn)證[J];計(jì)算機(jī)工程;2006年22期

2 駱翔宇;軒愛成;沙宗魯;;基于時(shí)間自動(dòng)機(jī)的Web服務(wù)模型檢測(cè)[J];計(jì)算機(jī)科學(xué);2010年08期

3 程廣金;繆淮扣;方明科;梅佳;氋洪皓;;基于XML的Web應(yīng)用模型抽取[J];計(jì)算機(jī)科學(xué);2011年09期

4 王建峰;;基于時(shí)間自動(dòng)機(jī)的入侵檢測(cè)系統(tǒng)的設(shè)計(jì)[J];咸寧學(xué)院學(xué)報(bào);2008年03期

5 何亞麗;張廣泉;王f;;基于XYZ/ADL的Web服務(wù)組合精化檢驗(yàn)[J];蘇州大學(xué)學(xué)報(bào)(自然科學(xué)版);2010年01期

6 駱翔宇;軒愛成;沙宗魯;;基于Verics的組合Web服務(wù)有界模型檢測(cè)[J];小型微型計(jì)算機(jī)系統(tǒng);2011年03期

7 張澤莉,馬華東;簡(jiǎn)單網(wǎng)絡(luò)支付協(xié)議的形式模型[J];北京郵電大學(xué)學(xué)報(bào);2002年04期

8 郭華;莊雷;張習(xí)勇;李舟軍;;基于模型檢測(cè)的多輪FR協(xié)議驗(yàn)證[J];計(jì)算機(jī)科學(xué);2008年05期

9 張廣泉;戎玫;朱雪陽(yáng);何亞麗;石慧娟;;基于XYZ/ADL的Web服務(wù)組合描述與驗(yàn)證[J];電子學(xué)報(bào);2011年S1期

10 楊秋偉;周潔;唐卓;劉玲;;帶時(shí)間特性的自動(dòng)信任協(xié)商[J];計(jì)算機(jī)應(yīng)用研究;2010年06期

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫(kù) 前1條

1 余興超;馬爭(zhēng)先;王玉斌;董榮勝;;基于UPPAAL的簡(jiǎn)單網(wǎng)絡(luò)支付協(xié)議形式化驗(yàn)證[A];廣西計(jì)算機(jī)學(xué)會(huì)2010年學(xué)術(shù)年會(huì)論文集[C];2010年

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前2條

1 莊雷;基于Gnutella協(xié)議的Peer-to-Peer網(wǎng)絡(luò)研究及其協(xié)議驗(yàn)證[D];中國(guó)人民解放軍信息工程大學(xué);2004年

2 易平;移動(dòng)Ad Hoc網(wǎng)絡(luò)入侵檢測(cè)與主動(dòng)響應(yīng)機(jī)制研究[D];復(fù)旦大學(xué);2005年

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前8條

1 王從銀;FR-Gnet網(wǎng)絡(luò)模型及其實(shí)現(xiàn)方案[D];鄭州大學(xué);2004年

2 劉金亮;基于時(shí)間自動(dòng)機(jī)的可生存性評(píng)估方法研究[D];大連理工大學(xué);2009年

3 何亞麗;基于XYZ/ADL的Web服務(wù)組合驗(yàn)證研究[D];蘇州大學(xué);2010年

4 丁秋峰;一種電子數(shù)據(jù)可信取證形式化模型[D];南京郵電大學(xué);2012年

5 夏洋洋;異步交互的Web服務(wù)建模與相容性檢測(cè)[D];南京航空航天大學(xué);2012年

6 周潔;帶時(shí)間特性的自動(dòng)信任協(xié)商模型研究[D];湖南大學(xué);2012年

7 計(jì)宏霖;基于UPPAAL的電子商務(wù)協(xié)議安全性分析[D];解放軍信息工程大學(xué);2008年

8 馬生;有窮機(jī)和邏輯結(jié)合的電子商務(wù)協(xié)議分析方法[D];燕山大學(xué);2012年

，

本文編號(hào)：985498