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

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

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

【參考文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

【共引文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3 陳海明;崔莉;謝開斌;;物聯(lián)網(wǎng)體系結(jié)構(gòu)與實(shí)現(xiàn)方法的比較研究[J];計(jì)算機(jī)學(xué)報(bào);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 吉鳴;黃志球;祝義;王珊珊;沈國(guó)華;;基于MDA的實(shí)時(shí)軟件資源建模與模型轉(zhuǎn)換的方法[J];計(jì)算機(jī)科學(xué);2011年08期

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

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

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

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

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

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

中國(guó)重要報(bào)紙全文數(shù)據(jù)庫(kù) 前10條

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

2 王紹斌;嵌入式軟件是個(gè)大市場(chǎng)[N];中國(guó)電子報(bào);2004年

3 周嫻;大連嵌入式軟件走向黃金期[N];中國(guó)電子報(bào);2004年

4 記者 楊慶廣;中國(guó)力量謀劃嵌入式軟件[N];中國(guó)電子報(bào);2005年

5 黃志敏;以嵌入式軟件技術(shù)帶動(dòng)軟件產(chǎn)業(yè)大發(fā)展[N];大連日?qǐng)?bào);2005年

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

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

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

9 ;韓國(guó)嵌入式軟件市場(chǎng)掃描[N];中國(guó)計(jì)算機(jī)報(bào);2004年

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號(hào)：1166450