本文關(guān)鍵詞：基于模型檢查的嵌入式軟件構(gòu)件化分析與驗證

  更多相關(guān)文章： 模型檢查 嵌入式軟件 構(gòu)件化 SMV

【摘要】：對嵌入式軟件構(gòu)件化進行準(zhǔn)確分析與驗證,能夠為嵌入式系統(tǒng)安全、穩(wěn)定的運行提供保障。提出一種基于模型檢查的嵌入式軟件構(gòu)件化分析與驗證方法。設(shè)計一種用于檢查軟件構(gòu)件的模型,為嵌入式軟件構(gòu)件化分析與驗證提供理論基礎(chǔ);將嵌入式軟件系統(tǒng)模型用SMV語言的形式表達,利用SMV模型檢查工具實現(xiàn)對嵌入式軟件運行狀態(tài)的分析與檢驗。實驗結(jié)果表明,該模型能夠?qū)η度胧杰浖䴓?gòu)件化的非功能性方面的設(shè)計要求進行準(zhǔn)確分析與驗證,為嵌入式系統(tǒng)安全穩(wěn)定的運行提供了保障。
【作者單位】： 成都醫(yī)學(xué)院人文信息管理學(xué)院;
【基金】：四川省教育廳項目(14ZB0241)
【分類號】：TP311.52
【正文快照】： 嵌入式系統(tǒng)各種功能的實現(xiàn)都離不開軟件[1],軟件具有極其重要的意義[2],它是影響嵌入式系統(tǒng)穩(wěn)定運行的關(guān)鍵因素,一旦關(guān)鍵部位中嵌入式系統(tǒng)的軟件失效[3],輕則造成財產(chǎn)損失,重則使生命受到威脅[4]。與PC機中的軟件相比,嵌入式系統(tǒng)中的軟件既要滿足其功能性設(shè)計要求[5],又要滿足

【參考文獻】

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

1 胡寧;葉宏;;嵌入式操作系統(tǒng)的形式化驗證方法[J];航空計算技術(shù);2015年02期

2 黃傳林;黃志球;胡軍;徐丙鳳;曲長亮;;基于擴展SysML活動圖的嵌入式系統(tǒng)設(shè)計安全性驗證方法研究[J];小型微型計算機系統(tǒng);2015年03期

3 符寧;杜承烈;李建良;劉志強;彭寒;;AADL分級調(diào)度模型的分析與驗證[J];計算機研究與發(fā)展;2015年01期

4 王鋒;張弛;;構(gòu)件化嵌入式軟件設(shè)計模型驗證工具的研究[J];通訊世界;2014年21期

5 黃菲;;嵌入式實時軟件的構(gòu)件化開發(fā)技術(shù)探究[J];信息技術(shù)與信息化;2014年10期

6 謝開斌;陳海明;崔莉;;物聯(lián)網(wǎng)軟件體系結(jié)構(gòu)中的感執(zhí)模型的求精[J];軟件學(xué)報;2014年08期

7 趙競雄;;嵌入式系統(tǒng)威脅與風(fēng)險評估過程仿真分析[J];計算機仿真;2014年04期

8 王博;白曉穎;賀飛;Xiaoyu SONG;;可組合嵌入式軟件建模與驗證技術(shù)研究綜述[J];軟件學(xué)報;2014年02期

9 白海洋;李靜;趙娜;;基于時間自動機的嵌入式軟件模型可調(diào)度性驗證[J];計算機工程與科學(xué);2013年03期

【共引文獻】

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

1 聶捷楠;;基于模型檢查的嵌入式軟件構(gòu)件化分析與驗證[J];現(xiàn)代電子技術(shù);2016年24期

2 陸陳;黃志球;闞雙龍;曹德建;黃傳林;;基于八邊形抽象域的襟縫翼控制系統(tǒng)安全性分析[J];小型微型計算機系統(tǒng);2016年05期

3 鄧雪峰;孫瑞志;聶娟;王文狄;史銀雪;;基于時間自動機的溫室環(huán)境監(jiān)控物聯(lián)網(wǎng)系統(tǒng)建模[J];農(nóng)業(yè)機械學(xué)報;2016年07期

4 李琪;;嵌入式軟件開放式開發(fā)技術(shù)分析[J];智能城市;2016年03期

5 李愛萍;馬俊偉;段利國;;智能家居平臺構(gòu)件適應(yīng)與協(xié)同模型及形式化分析[J];太原理工大學(xué)學(xué)報;2016年02期

6 陳宏君;王國棟;;組件系統(tǒng)接口匹配識別方案和應(yīng)用[J];計算機技術(shù)與發(fā)展;2016年02期

7 李靜;沈?qū)幟?白海洋;周培云;;基于時間自動機的嵌入式系統(tǒng)AADL模型可調(diào)度性驗證[J];東南大學(xué)學(xué)報(自然科學(xué)版);2015年06期

8 沈亮;;嵌入式軟件的測試方法與技術(shù)[J];數(shù)字技術(shù)與應(yīng)用;2015年11期

9 師麗斌;李蜀瑜;;基于ARINC 653標(biāo)準(zhǔn)的嵌入式構(gòu)件元模型研究[J];電子設(shè)計工程;2015年21期

10 李越;;計算機嵌入式軟件構(gòu)件提取與組裝技術(shù)[J];中國新通信;2015年19期

【二級參考文獻】

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

1 謝開斌;陳海明;崔莉;;PMDA:一種物理模型驅(qū)動的物聯(lián)網(wǎng)軟件體系結(jié)構(gòu)[J];計算機研究與發(fā)展;2013年06期

2 姬莉霞;馬建紅;;基于時間自動機的UML模型轉(zhuǎn)換與驗證研究[J];鄭州大學(xué)學(xué)報(理學(xué)版);2013年01期

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

4 周宇;Luciano Baresi;Matteo Rossi;;Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata[J];Journal of Computer Science & Technology;2013年01期

5 吉鳴;黃志球;祝義;王珊珊;沈國華;;基于MDA的實時軟件資源建模與模型轉(zhuǎn)換的方法[J];計算機科學(xué);2011年08期

6 劉亞萍;黃志球;祝義;;基于元建模的實時系統(tǒng)模型轉(zhuǎn)換方法研究[J];小型微型計算機系統(tǒng);2010年11期

7 楊志斌;皮磊;胡凱;顧宗華;馬殿富;;復(fù)雜嵌入式實時系統(tǒng)體系結(jié)構(gòu)設(shè)計與分析語言:AADL[J];軟件學(xué)報;2010年05期

8 向凱全;李雄偉;王紅勝;張陽;;可重用構(gòu)件的軟件開發(fā)技術(shù)研究[J];河北科技大學(xué)學(xué)報;2010年01期

9 劉倩;桂盛霖;李允;羅蕾;;基于UPPAAL的AADL模型可調(diào)度性驗證[J];計算機應(yīng)用;2009年07期

10 張?zhí)?Frédéric JOUAULT;Christian ATTIOGB;Jean BZIVIN;李宣東;;基于MDE的異構(gòu)模型轉(zhuǎn)換:從MARTE模型到FIACRE模型[J];軟件學(xué)報;2009年02期

【相似文獻】

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

1 葉雨新;“嵌入式”與我們的機遇──發(fā)展嵌入式軟件的幾點思考[J];軟件世界;2001年03期

2 李巖;嵌入式軟件技術(shù)的現(xiàn)狀與發(fā)展動向[J];遼寧高職學(xué)報;2002年03期

3 鐘錫昌;嵌入式軟件面臨良好發(fā)展機遇[J];科技廣場;2003年06期

4 蘇珊 ,依然;好產(chǎn)品是賣出來的——“道系統(tǒng)”自主知識產(chǎn)權(quán)的嵌入式軟件產(chǎn)品[J];電子設(shè)計應(yīng)用;2003年Z1期

5 王繼春;嵌入式軟件及其應(yīng)用領(lǐng)域與發(fā)展趨勢[J];信息技術(shù)與信息化;2004年04期

6 方天選;淺談嵌入式軟件[J];山西電子技術(shù);2004年05期

7 吳朝暉;;嵌入式軟件發(fā)展的十個觀點[J];計算機教育;2005年05期

8 彭敏;嵌入式軟件:人才仍是關(guān)鍵[J];軟件世界;2005年11期

9 吳朝暉;嵌入式軟件發(fā)展趨勢[J];電子產(chǎn)品世界;2005年03期

10 ;嵌入式軟件,“嵌入”了什么?[J];軟件世界;2006年10期

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

1 蘇運霖;;智能嵌入式軟件初探[A];第十屆全國電工數(shù)學(xué)學(xué)術(shù)年會論文集[C];2005年

2 劉華;;通信設(shè)備嵌入式軟件可靠性研究[A];第九屆中國通信學(xué)會學(xué)術(shù)年會論文集[C];2012年

3 楊云松;孫旭光;梅文華;;嵌入式軟件的加解密分析[A];第六屆全國計算機應(yīng)用聯(lián)合學(xué)術(shù)會議論文集[C];2002年

4 曹松;李慧軍;惠平;;航天嵌入式軟件的發(fā)展趨勢[A];中國空間科學(xué)學(xué)會空間探測專業(yè)委員會第十六次學(xué)術(shù)會議論文集（下）[C];2003年

5 貢巖;黃琳;;指揮自動化系統(tǒng)嵌入式軟件可靠性評估[A];中國電子學(xué)會可靠性分會第十三屆學(xué)術(shù)年會論文選[C];2006年

6 張志剛;;基于動態(tài)跟蹤模式的軍用嵌入式軟件需求質(zhì)量改進方法研究[A];質(zhì)量——持續(xù)發(fā)展的源動力：中國質(zhì)量學(xué)術(shù)與創(chuàng)新論壇論文集（下）[C];2010年

7 畢經(jīng)存;;一種實用的嵌入式軟件測試方法研究[A];2008’“先進集成技術(shù)”院士論壇暨第二屆儀表、自動化與先進集成技術(shù)大會論文集[C];2008年

8 劉旭;謝家強;林嵐;;建立嵌入式軟件出口統(tǒng)計目錄的探討[A];國際服務(wù)貿(mào)易評論（總第7輯）[C];2013年

9 范東麗;孫長嵩;;嵌入式軟件的測試策略初探[A];2006北京地區(qū)高校研究生學(xué)術(shù)交流會——通信與信息技術(shù)會議論文集（下）[C];2006年

10 江乾坤;王澤霞;;嵌入式軟件產(chǎn)品銷售收入核算方法研究[A];中國會計學(xué)會高等工科院校分會2006年學(xué)術(shù)年會暨第十三屆年會論文集[C];2006年

中國重要報紙全文數(shù)據(jù)庫 前10條

1 孫愛民;倪光南：嵌入式軟件是邁向創(chuàng)造的契機[N];中國電子報;2004年

2 王紹斌;嵌入式軟件是個大市場[N];中國電子報;2004年

3 周嫻;大連嵌入式軟件走向黃金期[N];中國電子報;2004年

4 記者 楊慶廣;中國力量謀劃嵌入式軟件[N];中國電子報;2005年

5 黃志敏;以嵌入式軟件技術(shù)帶動軟件產(chǎn)業(yè)大發(fā)展[N];大連日報;2005年

6 顧汶;嵌入式軟件成熱點 行業(yè)標(biāo)準(zhǔn)亟待出臺[N];中國高新技術(shù)產(chǎn)業(yè)導(dǎo)報;2005年

7 張偉;嵌入式軟件產(chǎn)業(yè) 熱豆腐不能急吃[N];中國高新技術(shù)產(chǎn)業(yè)導(dǎo)報;2005年

8 顧衛(wèi)民;嵌入式軟件契機乍現(xiàn) 高新區(qū)一馬當(dāng)先嗑[N];中國高新技術(shù)產(chǎn)業(yè)導(dǎo)報;2005年

9 ;韓國嵌入式軟件市場掃描[N];中國計算機報;2004年

10 霍峰 孟繁;高新區(qū)全力打造嵌入式軟件產(chǎn)業(yè)[N];青島日報;2005年

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

1 徐丙鳳;構(gòu)件化嵌入式軟件安全性分析方法研究[D];南京航空航天大學(xué);2014年

2 孫福振;基于模型檢查的嵌入式軟件構(gòu)件化分析與驗證[D];北京理工大學(xué);2015年

3 鄧阿群;面向方面技術(shù)在大規(guī)模嵌入式軟件中的應(yīng)用[D];浙江大學(xué);2007年

4 夏一行;面向數(shù)字化儀器設(shè)備的嵌入式軟件應(yīng)用框架研究[D];浙江大學(xué);2007年

5 郭兵;嵌入式軟件開放式集成開發(fā)平臺體系結(jié)構(gòu)研究[D];電子科技大學(xué);2002年

6 祝義;嵌入式軟件需求規(guī)約到軟件體系結(jié)構(gòu)模型的轉(zhuǎn)換研究[D];南京航空航天大學(xué);2011年

7 高志剛;基于模型的汽車電子軟件綜合方法研究[D];浙江大學(xué);2008年

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

1 郭旺;嵌入式軟件覆蓋測試通用技術(shù)研究[D];西南大學(xué);2015年

2 朱晏慶;衛(wèi)星控制系統(tǒng)嵌入式軟件虛擬化測試平臺技術(shù)研究[D];上海交通大學(xué);2014年

3 朱柯潤;基于ARM的船用雷達嵌入式軟件可靠性研究[D];電子科技大學(xué);2014年

4 林紅;實時系統(tǒng)嵌入式軟件可靠性分析與測試案例研究[D];電子科技大學(xué);2014年

5 趙少杰;數(shù)字示波器接口擴展模塊嵌入式軟件的設(shè)計與實現(xiàn)[D];電子科技大學(xué);2014年

6 郭春榮;嵌入式Linux軟件構(gòu)建工具的設(shè)計與實現(xiàn)[D];中國科學(xué)院大學(xué)(工程管理與信息技術(shù)學(xué)院);2015年

7 郝旭;面向C語言的嵌入式軟件能耗估算方法的研究與設(shè)計[D];東北大學(xué);2014年

8 肖前遠(yuǎn);航空嵌入式軟件全數(shù)字仿真測試技術(shù)研究[D];南京航空航天大學(xué);2010年

9 姜兆義;星載嵌入式軟件集成開發(fā)環(huán)境設(shè)計與關(guān)鍵技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2004年

10 張濤;嵌入式軟件模擬測試平臺中符號測試命令語言[D];西北工業(yè)大學(xué);2005年

，

本文編號：1166450