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

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

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

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

【部分圖文】：

Communication的接口自動機模型

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

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

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

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



本文編號：2911911