發(fā)布時(shí)間：2020-12-12 05:08

　　現(xiàn)代復(fù)雜嵌入式軟件系統(tǒng)的高可靠性需要有效的基于模型的設(shè)計(jì)與分析技術(shù)。由于嵌入軟件具有極高的可靠性、嚴(yán)格的實(shí)時(shí)性以及資源、能耗使用的受限性,使得保證系統(tǒng)設(shè)計(jì)滿足給定的功能規(guī)約以及滿足非功能方面的嚴(yán)格限制成為嵌入式計(jì)算領(lǐng)域中的重要研究課題。傳統(tǒng)的嵌入式軟件可靠性保障技術(shù)主要關(guān)注于系統(tǒng)開(kāi)發(fā)后期,而在系統(tǒng)設(shè)計(jì)前期缺乏有效工具對(duì)系統(tǒng)設(shè)計(jì)的功能性質(zhì)以及非功能性質(zhì)進(jìn)行分析與驗(yàn)證。本文以接口自動(dòng)機(jī)及其擴(kuò)展模型作為構(gòu)件化嵌入式軟件的設(shè)計(jì)模型,以UML順序圖描述基于場(chǎng)景的功能規(guī)約,對(duì)基于接口自動(dòng)機(jī)及其擴(kuò)展模型的多個(gè)模型檢驗(yàn)抽象算法進(jìn)行分析且設(shè)計(jì)相應(yīng)的算法實(shí)現(xiàn)框架。進(jìn)而在Eclipse平臺(tái)上設(shè)計(jì)并實(shí)現(xiàn)了一個(gè)基于接口自動(dòng)機(jī)模型的構(gòu)件化嵌入式軟件設(shè)計(jì)的形式化驗(yàn)證原型工具T-CBESD（Tool for Component-Based Embedded Software Design）。該工具直接使用UML順序圖模型作為系統(tǒng)規(guī)約,可以檢驗(yàn)系統(tǒng)設(shè)計(jì)模型與場(chǎng)景規(guī)約之間多種行為一致性問(wèn)題;并使用消息事件的時(shí)間約束不等式,檢驗(yàn)實(shí)時(shí)接口自動(dòng)機(jī)網(wǎng)絡(luò)與帶時(shí)間約束的順序圖模型之間的實(shí)時(shí)行為一致性問(wèn)題;另外,對(duì)非實(shí)時(shí)資源使用相關(guān)性... 

【文章來(lái)源】：南京航空航天大學(xué)江蘇省 211工程院校

【文章頁(yè)數(shù)】：76 頁(yè)

【學(xué)位級(jí)別】：碩士

【部分圖文】：

Communication的接口自動(dòng)機(jī)模型

從信道返回的ack；然后向調(diào)用者返回通信失�。篺ail。從圖中可以看出，Comm入動(dòng)作msg僅在狀態(tài)0可以接受，在其余用了msg方法，則在下一次調(diào)用msg之前nication被另外一個(gè)構(gòu)件User使用(如圖2.2失敗的處理。這樣，總是返回ok就成為了圖 2.1 Communication 的接口自動(dòng)機(jī)模型

圖 3.1 TCAS 系統(tǒng)中飛行沖突探測(cè)場(chǎng)景的 UML 順序圖中的消息發(fā)送以及消息的接收都使用事件來(lái)表示。不失一般性，假定每或多個(gè)可視序列，每個(gè)可視序列中的元素都是一個(gè)事件對(duì)(e1, e2) ；表示生。在本文中，暫不考慮帶選擇分支的順序圖。在圖中只要當(dāng)出現(xiàn)滿足被視為在事件e2之前發(fā)生：果關(guān)系：e1為消息發(fā)送事件，e2為此消息對(duì)應(yīng)的接收事件。制關(guān)系：在同一個(gè)構(gòu)件的生命線軸上，事件e1出現(xiàn)于事件e2的上方，且e2事件順序表明一個(gè)發(fā)送事件可以等待其他事件的發(fā)生。但是一個(gè)構(gòu)件只件的時(shí)間先后，對(duì)于接收消息事件，由于系統(tǒng)的底層結(jié)構(gòu)和消息傳送的收消息的時(shí)間也是不確定的，所以對(duì)消息接收事件的發(fā)生的順序沒(méi)有做O順序關(guān)系：在同一個(gè)構(gòu)件的生命線軸上，接收事件e1出現(xiàn)于接收事件的發(fā)送事件'1e 和'2e 同時(shí)出現(xiàn)在另外一個(gè)構(gòu)件的生命線軸上，且'1e 位置高序圖中的任何消息而言，可能是同步的，也可能是異步的。異步的消息則在其發(fā)送和接收事件之間不會(huì)有時(shí)間延遲。本文中假定順序圖中的消

【參考文獻(xiàn)】：
期刊論文
[1]構(gòu)件化嵌入式軟件設(shè)計(jì)的能耗性質(zhì)分析與驗(yàn)證[J]. 曹東,胡軍,徐丙鳳.  南京理工大學(xué)學(xué)報(bào)(自然科學(xué)版). 2009(01)
[2]網(wǎng)構(gòu)軟件的資源自適應(yīng)性的形式化分析與驗(yàn)證[J]. 胡軍,黃志球,曹東,徐丙鳳.  軟件學(xué)報(bào). 2008(05)
[3]基于場(chǎng)景規(guī)約的構(gòu)件式系統(tǒng)設(shè)計(jì)分析與驗(yàn)證[J]. 胡軍,于笑豐,張巖,王林章,李宣東,鄭國(guó)梁.  計(jì)算機(jī)學(xué)報(bào). 2006(04)
[4]基于場(chǎng)景構(gòu)件式實(shí)時(shí)軟件設(shè)計(jì)的一致性檢驗(yàn)[J]. 胡軍,于笑豐,張巖,李宣東,鄭國(guó)梁.  軟件學(xué)報(bào). 2006(01)
[5]嵌入式軟件建模、實(shí)現(xiàn)與驗(yàn)證:研究與進(jìn)展[J]. 胡軍,張巖,于笑豐,王林章,李宣東,鄭國(guó)梁.  計(jì)算機(jī)科學(xué). 2005(12)
[6]接口自動(dòng)機(jī)——一種用于組件組合的形式系統(tǒng)[J]. 張巖,胡軍,于笑豐,李宣東,鄭國(guó)梁.  計(jì)算機(jī)科學(xué). 2005(11)
[7]軟件復(fù)用與軟件構(gòu)件技術(shù)[J]. 楊芙清,梅宏,李克勤.  電子學(xué)報(bào). 1999(02)

博士論文
[1]構(gòu)件化嵌入式軟件設(shè)計(jì)的分析與驗(yàn)證[D]. 胡軍.南京大學(xué) 2005



本文編號(hào)：2911911