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

  更多相關(guān)文章： 信息物理融合系統(tǒng) 面向服務 模型驗證 時間自動機 Uppaal

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

【參考文獻】

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

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

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

3 李力行;金芝;李戈;;基于時間自動機的物聯(lián)網(wǎng)服務建模和驗證[J];計算機學報;2011年08期

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

【共引文獻】

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

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

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

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

4 王樂達;;倉庫管理信息物理融合系統(tǒng)[J];計算機光盤軟件與應用;2014年03期

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

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

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

8 周宇;胡軍;葛季棟;;一種層次式時間自動機模型檢測方法[J];計算機應用與軟件;2012年11期

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

10 黎曉波;網(wǎng)絡拓撲快速變化的Ad-Hoc路由協(xié)議研究[D];北京郵電大學;2013年

【二級參考文獻】

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

1 侯麗珊;金芝;吳步丹;;需求驅(qū)動的Web服務建模及其驗證:一個基于本體的方法[J];中國科學E輯:信息科學;2006年10期

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

【相似文獻】

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

1 高冠龍;周清雷;;時間自動機與網(wǎng)絡協(xié)議驗證[J];計算機工程;2006年22期

2 駱翔宇;軒愛成;沙宗魯;;基于時間自動機的Web服務模型檢測[J];計算機科學;2010年08期

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

4 王建峰;;基于時間自動機的入侵檢測系統(tǒng)的設計[J];咸寧學院學報;2008年03期

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

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

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

8 郭華;莊雷;張習勇;李舟軍;;基于模型檢測的多輪FR協(xié)議驗證[J];計算機科學;2008年05期

9 張廣泉;戎玫;朱雪陽;何亞麗;石慧娟;;基于XYZ/ADL的Web服務組合描述與驗證[J];電子學報;2011年S1期

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

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

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

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

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

2 易平;移動Ad Hoc網(wǎng)絡入侵檢測與主動響應機制研究[D];復旦大學;2005年

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

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

2 劉金亮;基于時間自動機的可生存性評估方法研究[D];大連理工大學;2009年

3 何亞麗;基于XYZ/ADL的Web服務組合驗證研究[D];蘇州大學;2010年

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

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

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

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

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

，

本文編號：985498