【摘要】：基于模型的設(shè)計與分析技術(shù)是現(xiàn)代復(fù)雜嵌入式軟件系統(tǒng)高可靠性的重要保障手段。與一般的軟件系統(tǒng)相比,嵌入式軟件具有極高的可靠性、嚴格的實時性以及可使用資源的受限性、滿足特定領(lǐng)域等要求。如何保證系統(tǒng)設(shè)計滿足給定的功能規(guī)約,以及滿足實時、資源、能耗等非功能方面的嚴格限制,提高軟件的可靠性已成為嵌入式計算領(lǐng)域中的重要研究課題。 傳統(tǒng)的嵌入式軟件可靠性保障技術(shù)主要關(guān)注于系統(tǒng)開發(fā)后期,而在軟件設(shè)計與分析的前期階段還缺乏有效的方法和工具來支持對系統(tǒng)設(shè)計的分析與驗證。本文對基于即時驗證的嵌入式軟件驗證理論和技術(shù)進行深入研究,采用UML交互概觀圖模型描述基于場景的系統(tǒng)規(guī)約,以接口自動機及其擴展模型作為嵌入式軟件系統(tǒng)設(shè)計模型,設(shè)計相應(yīng)的即時驗證算法(On-the-fly verification algorithm),對嵌入式軟件設(shè)計階段有關(guān)系統(tǒng)動態(tài)行為的功能及非功能屬性進行形式化分析與驗證。 根據(jù)所設(shè)計的即時驗證算法,在Eclipse平臺上對一個構(gòu)件化嵌入式軟件設(shè)計模型的原型驗證工具T-CBESD進行擴展設(shè)計與實現(xiàn),以提高原型工具的驗證效率與實用性。主要工作包括:擴展工具的輸入接口,改進工具的核心算法,實例研究,證明即時驗證算法的高效性和準確性。擴展后的工具為現(xiàn)代復(fù)雜嵌入式軟件系統(tǒng)設(shè)計提供了有效的基于模型的分析與驗證工具。
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2010
【分類號】：TP368.1
【圖文】：

南京航空航天大學(xué)碩士學(xué)位論文接口。但工業(yè)界已有一些比較成熟的形式化圖形工具，提供了繪制基AP[44]。JFLAP為我們提供了方便易用的有限自動機建模接口，并提供一些文本和標簽的功能。為此，對于接口自動機的圖形化建模而言，P。其原因有二：首先，JFLAP是基于Java的開源系統(tǒng)，很容易集成到P提供了良好的建立有限自動機的建模機制，雖然無法直接通過JFLA但是可以通過在JFLAP的自動機模型中添加合適的語法結(jié)構(gòu)來表達接義信息，并通過進一步的處理來獲得滿足T-CBESD輸入格式要求的模建立能耗接口自動機模型界面。

圖 3.1 圖書館借書系統(tǒng) UML 交互概觀圖模型動圖和順序圖的結(jié)合體，直觀地表達一組相關(guān)順序圖圖和順序圖的形式化說明的基礎(chǔ)上給出的。以下給出觀圖、實時交互概觀圖的形式化定義：語義如下[46]：：一個活動圖是一個六元組，D=(A，T，F(xiàn)，G，ai，…，am｝是一個有窮的活動狀態(tài)集；…，tn｝是一個有限完成躍遷集；∪T×A）是流關(guān)系； 的條件表達式；活動狀態(tài)，af∈A 是終止活動狀態(tài)； t 滿足ai，t）∈F；T，（tj，ai） F 且（af，tj） F。語義如下[9]：

南京航空航天大學(xué)碩士學(xué)位論文十分必要的。對于交互概觀圖的建模而言，目前還不存在提供直接繪制化建模工具。但是我們發(fā)現(xiàn)工具 Topcased[47]提供了一種間接繪制的方e 插件，支持多種 UML 模型圖的繪制，提供了繪制活動圖并可以用相關(guān)功能。即：可以在 Topcased 中，先繪制活動圖對系統(tǒng)運行流程進行建對活動圖中的一些關(guān)鍵節(jié)點進行細化，用于描述系統(tǒng)運行時的某個具體概觀圖描述系統(tǒng)規(guī)約的功能。因此，我們選擇 Topcased 作為 UML 交互模接口。圖 3.2 給出了 Topcased 工具繪制規(guī)約模型的界面。

【參考文獻】

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

1 顏炯;王戟;陳火旺;;基于模型的軟件測試綜述[J];計算機科學(xué);2004年02期

2 胡軍;張巖;于笑豐;王林章;李宣東;鄭國梁;;嵌入式軟件建模、實現(xiàn)與驗證:研究與進展[J];計算機科學(xué);2005年12期

3 崔萌 ,李宣東 ,鄭國梁;UML實時活動圖的形式化分析[J];計算機學(xué)報;2004年03期

4 胡軍;于笑豐;張巖;王林章;李宣東;鄭國梁;;基于場景規(guī)約的構(gòu)件式系統(tǒng)設(shè)計分析與驗證[J];計算機學(xué)報;2006年04期

5 曹東;胡軍;徐丙鳳;;構(gòu)件化嵌入式軟件設(shè)計的能耗性質(zhì)分析與驗證[J];南京理工大學(xué)學(xué)報(自然科學(xué)版);2009年01期

6 胡軍;于笑豐;張巖;李宣東;鄭國梁;;基于場景構(gòu)件式實時軟件設(shè)計的一致性檢驗[J];軟件學(xué)報;2006年01期

7 胡軍;黃志球;曹東;徐丙鳳;;網(wǎng)構(gòu)軟件的資源自適應(yīng)性的形式化分析與驗證[J];軟件學(xué)報;2008年05期

相關(guān)博士學(xué)位論文 前1條

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

本文編號：2804439