發(fā)布時(shí)間：2020-08-26 00:58

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

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

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

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

【參考文獻(xiàn)】

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

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

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

3 崔萌 ,李宣東 ,鄭國(guó)梁;UML實(shí)時(shí)活動(dòng)圖的形式化分析[J];計(jì)算機(jī)學(xué)報(bào);2004年03期

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

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

6 胡軍;于笑豐;張巖;李宣東;鄭國(guó)梁;;基于場(chǎng)景構(gòu)件式實(shí)時(shí)軟件設(shè)計(jì)的一致性檢驗(yàn)[J];軟件學(xué)報(bào);2006年01期

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

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

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

本文編號(hào)：2804439