本文選題：嵌入式軟件　切入點(diǎn)：可信性　出處：《南京航空航天大學(xué)》2016年博士論文　論文類型：學(xué)位論文

【摘要】：嵌入式軟件在關(guān)鍵領(lǐng)域的廣泛應(yīng)用使其對(duì)可信性的需求遠(yuǎn)遠(yuǎn)高于一般軟件。由于嵌入式軟件在體系架構(gòu)、資源限制、應(yīng)用環(huán)境等方面的特殊性,以及近年來復(fù)雜化、規(guī)�；c開放化的發(fā)展趨勢(shì),保障和評(píng)估嵌入式軟件的可信性已成為國(guó)內(nèi)外越來越關(guān)注的研究熱點(diǎn)之一。在嵌入式軟件開發(fā)早期對(duì)其可信性進(jìn)行分析、驗(yàn)證與評(píng)估,能夠減少潛在的軟件缺陷,從而降低后期測(cè)試與維護(hù)的成本。本文立足于可信嵌入式軟件的建模與驗(yàn)證問題,旨在建立基于模型驅(qū)動(dòng)的嵌入式軟件建模與驗(yàn)證集成框架;采用Z語(yǔ)言為該框架提供形式化語(yǔ)義,針對(duì)嵌入式軟件可信屬性開展建模、驗(yàn)證與評(píng)估技術(shù)的研究;設(shè)計(jì)并實(shí)現(xiàn)了相應(yīng)的原型系統(tǒng),在嵌入式軟件實(shí)例上進(jìn)行應(yīng)用研究。論文研究工作的主要?jiǎng)?chuàng)新性成果如下:(1)根據(jù)嵌入式軟件的可信需求,提出了一種嵌入式軟件形式化模型Z-MARTE,包括Z-MARTE時(shí)間模型、結(jié)構(gòu)模型與行為模型。與現(xiàn)有模型相比,Z-MARTE是一種靜態(tài)結(jié)構(gòu)與動(dòng)態(tài)行為的綜合模型,能夠同時(shí)描述嵌入式軟件功能結(jié)構(gòu)、時(shí)序行為以及可信約束。在Z-MARTE模型中引入了可信構(gòu)造型的概念,通過對(duì)可信構(gòu)造型的聲明與約束,能夠描述包括數(shù)據(jù)約束與時(shí)間約束在內(nèi)的各類可信約束,為嵌入式軟件可信性的驗(yàn)證與評(píng)估提供形式化語(yǔ)義基礎(chǔ)。(2)為了對(duì)Z-MARTE模型描述的可信約束進(jìn)行自動(dòng)驗(yàn)證,提出了一種基于模型檢測(cè)技術(shù)的嵌入式軟件可信驗(yàn)證方法。首先,給出了有限域上Z-MARTE行為模型的語(yǔ)義解釋,為模型檢測(cè)方法提供了行為語(yǔ)義基礎(chǔ);其次,擴(kuò)展了CTL的語(yǔ)法與語(yǔ)義,定義了一種描述嵌入式軟件可信性質(zhì)的時(shí)序邏輯公式ZMTL;最后,設(shè)計(jì)了有限域Z-MARTE行為模型上的模型檢測(cè)算法FZMCA,能夠在有限域內(nèi)對(duì)Z-MARTE模型中的實(shí)時(shí)性、安全性等可信性質(zhì)進(jìn)行自動(dòng)驗(yàn)證。(3)為了對(duì)Z-MARTE模型進(jìn)行進(jìn)一步的評(píng)估與分析,提出了一種嵌入式軟件風(fēng)險(xiǎn)評(píng)估方法RAMES。首先,對(duì)Z-MARTE結(jié)構(gòu)模型進(jìn)行精化與擴(kuò)展,提出了一種嵌入式軟件對(duì)象-消息-角色模型OMR;在此基礎(chǔ)上提出了風(fēng)險(xiǎn)分析算法RAOMR,以O(shè)MR模型中的嵌入式軟件對(duì)象為評(píng)估單位,以對(duì)象間的通信行為與軟件安全約束為評(píng)估依據(jù)進(jìn)行風(fēng)險(xiǎn)評(píng)估,并進(jìn)行了算法復(fù)雜度分析與實(shí)例研究。RAMES方法遵循ISO 31000標(biāo)準(zhǔn)的風(fēng)險(xiǎn)管理過程,其評(píng)估結(jié)果能夠指導(dǎo)嵌入式軟件設(shè)計(jì)模型中安全資源的合理分配。(4)在上述研究成果的基礎(chǔ)上,建立了一個(gè)嵌入式軟件可信性建模與驗(yàn)證集成框架,設(shè)計(jì)并初步實(shí)現(xiàn)了一個(gè)原型系統(tǒng)。在Eclipse平臺(tái)上初步實(shí)現(xiàn)了一個(gè)基于XSLT轉(zhuǎn)換技術(shù)的模型轉(zhuǎn)換工具ZMT,將半形式化建模環(huán)境Open Embe DD與形式化建模環(huán)境CZT進(jìn)行了集成;在VC 6.0平臺(tái)上,對(duì)Z-MARTE模型解析模塊、Z-MARTE行為模型生成模塊與FZMCA模型檢測(cè)模塊進(jìn)行了研究與實(shí)現(xiàn);最后,對(duì)原型系統(tǒng)的應(yīng)用技術(shù)進(jìn)行了研究。
[Abstract]:The widespread application of embedded software in key fields makes its demand for credibility much higher than that of general software. Due to the particularity of embedded software in architecture, resource limitation, application environment and so on, it is complicated in recent years. With the development of scale and openness, ensuring and evaluating the credibility of embedded software has become one of the research hotspots at home and abroad. In the early stage of embedded software development, the credibility of embedded software is analyzed, verified and evaluated. It can reduce the potential software defects and reduce the cost of later testing and maintenance. Based on the modeling and verification of trusted embedded software, this paper aims to build an integrated framework for modeling and verification of embedded software based on model-driven. Z language is used to provide formal semantics for the framework, modeling, verification and evaluation techniques for trusted attributes of embedded software are studied, and the corresponding prototype system is designed and implemented. The main innovative achievements of this paper are as follows: 1) according to the trusted requirement of embedded software, a formalized model of embedded software Z-MARTEincluding Z-MARTE time model is proposed. Compared with the existing models, Z-MARTE is a comprehensive model of static structure and dynamic behavior, which can describe the functional structure of embedded software at the same time. The concept of trusted constructive type is introduced into Z-MARTE model. By declaring and constraining trusted stereotype, we can describe all kinds of trusted constraints, including data constraint and time constraint. This paper provides a formal semantic basis for credibility verification and evaluation of embedded software. In order to automatically validate the trusted constraints described by Z-MARTE model, a method of trusted verification based on model checking technology is proposed. In this paper, the semantic interpretation of Z-MARTE behavior model over finite field is given, which provides the basis of behavioral semantics for model checking. Secondly, the syntax and semantics of CTL are extended to define a temporal logic formula that describes the trusted properties of embedded software. In order to evaluate and analyze the Z-MARTE model, a model detection algorithm named FZMCA based on the behavior model of Z-MARTE in finite domain is designed, which can automatically verify the real-time, security and other trusted properties of the Z-MARTE model in the finite domain. In this paper, a risk assessment method for embedded software, Rames, is proposed. Firstly, the Z-MARTE structure model is refined and extended. In this paper, an embedded software object-message role model (OMRs) is proposed, and a risk analysis algorithm, RAOMR-based, is proposed, which takes embedded software objects in OMR model as evaluation unit. Based on the communication behavior between objects and software security constraints, the risk assessment is carried out, and the algorithm complexity analysis and an example study are given. The method follows the ISO 31000 standard risk management process. The evaluation results can guide the rational allocation of security resources in the embedded software design model. Based on the above research results, an integrated framework for credibility modeling and verification of embedded software is established. A prototype system is designed and implemented preliminarily. A model transformation tool based on XSLT transformation technology is implemented on Eclipse platform. The semi-formal modeling environment Open Embe DD is integrated with formal modeling environment CZT. The Z-MARTE behavior model generation module and the FZMCA model detection module are studied and implemented. Finally, the application technology of the prototype system is studied.
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2016
【分類號(hào)】：TP311.5

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 鐘錫昌;嵌入式軟件現(xiàn)狀及發(fā)展趨勢(shì)[J];家用電器科技;2001年09期

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

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

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

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

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

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

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

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

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

相關(guān)會(huì)議論文 前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ān)重要報(bào)紙文章 前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ān)博士學(xué)位論文 前8條

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

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

3 倪思如;嵌入式軟件可信性建模與驗(yàn)證技術(shù)的研究及其應(yīng)用[D];南京航空航天大學(xué);2016年

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

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

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

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

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

相關(guān)碩士學(xué)位論文 前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語(yǔ)言的嵌入式軟件能耗估算方法的研究與設(shè)計(jì)[D];東北大學(xué);2014年

8 趙繁華;基于可信的某嵌入式軟件自動(dòng)化測(cè)試平臺(tái)的設(shè)計(jì)與實(shí)現(xiàn)[D];北京工業(yè)大學(xué);2015年

9 張漢青;基于授權(quán)芯片的認(rèn)證庫(kù)開發(fā)以及加密技術(shù)研究[D];華中科技大學(xué);2015年

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

，

本文編號(hào)：1633897