基于接口自動機的嵌入式軟件驗證技術(shù)及支撐工具研究

1、基于接口自動機的嵌入式軟件驗證技術(shù)及支撐工具研究    英文題名 Research on Interface Automata Based Embedded Software Verification Techniques and Supporting Tools  關(guān)鍵詞 嵌入式軟件設(shè)計; 構(gòu)件化設(shè)計; 軟件驗證; 接口自動機; UML; 模型檢驗工具; 英文關(guān)鍵詞 Embedded software design; Component-based design; Software verification; Interface Automa

2、ta; UML; Model checking tool; 中文摘要 現(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)行分析與驗證。 本文以接口自動機及其擴(kuò)展模型作為構(gòu)件化嵌入式軟件的設(shè)計模型,以UML順序圖描述基于場景的功能規(guī)約,對基于接口自動機及其擴(kuò)展模型的多個模型檢驗抽象算法進(jìn)行分析且設(shè)

3、計相應(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)性質(zhì)以及與時間相. 英文摘要 High reliability requirements of modern embedded s

4、oftware system need effective model-based techniques for system designs 摘要 4-5 ABSTRACT 5 圖表清單 8-10 注釋表 10-11 第一章 緒論 11-15     1.1 課題研究背景及意義 11-12     1.2 當(dāng)前研究現(xiàn)狀及選題依據(jù) 12-13     1.3 論文的研究內(nèi)容 13-15 第二章 接口自動機及其擴(kuò)展模型 15-22     2.1 接口自動機的非形式化描述以及形

5、式化定義 15-18         2.1.1 接口自動機的非形式化描述 15-17         2.1.2 接口自動機的形式化定義 17-18     2.2 接口自動機的擴(kuò)展模型 18-21         2.2.1 實時接口自動機模型 18-19         2.2.2

6、資源接口自動機模型 19-20         2.2.3 能耗接口自動機模型 20-21     2.3 本章小結(jié) 21-22 第三章 基于場景規(guī)約的驗證問題及抽象算法框架 22-34     3.1 UML 順序圖的形式化描述 22-25         3.1.1 UML 順序圖的形式化定義 22-24         3

7、.1.2 帶時間約束的UML 順序圖模型 24-25     3.2 接口自動機網(wǎng)絡(luò)模型與兼容可達(dá)圖 25-28         3.2.1 接口自動機網(wǎng)絡(luò)模型 25-28         3.2.2 兼容狀態(tài)空間的可達(dá)圖 28     3.3 關(guān)鍵問題以及相關(guān)抽象算法框架 28-33         3.3.1 非實時功能行為

8、驗證 28-30         3.3.2 實時功能行為驗證 30-31         3.3.3 資源性質(zhì)驗證 31-32         3.3.4 能耗性質(zhì)驗證 32-33     3.4 本章小結(jié) 33-34 第四章 T-CBESD體系結(jié)構(gòu)以及功能驗證模塊的設(shè)計與實現(xiàn) 34-47     4.1 現(xiàn)有模型驗證工具的分

9、析 34-36     4.2 T-CBESD開發(fā)及運行環(huán)境 36     4.3 T-CBESD體系結(jié)構(gòu)以及界面設(shè)計 36-40         4.3.1 T-CBESD體系結(jié)構(gòu) 36-38         4.3.2 T-CBESD界面設(shè)計 38-40     4.4 功能驗證模塊的設(shè)計與實現(xiàn) 40-46     

10、0;   4.4.1 功能驗證模塊的設(shè)計 40-41         4.4.2 功能驗證模塊輸入輸出接口的設(shè)計實現(xiàn) 41-42         4.4.3 UML 順序圖模型的輸入預(yù)處理 42-43         4.4.4 基本接口自動機組合模型的建立 43-44         4.4.5

11、非實時功能行為驗證算法的實現(xiàn) 44-46     4.5 本章小結(jié) 46-47 第五章 T-CBESD非功能性質(zhì)驗證模塊的設(shè)計與實現(xiàn) 47-58     5.1 非功能性質(zhì)驗證模塊的設(shè)計 47-48     5.2 實時驗證模塊的設(shè)計與實現(xiàn) 48-51         5.2.1 實時驗證模塊輸入輸出接口設(shè)計 48-49         5.2.2 帶時間約束的UML

12、 順序圖的輸入預(yù)處理 49-50         5.2.3 實時接口自動機組合模型的建立 50         5.2.4 實時功能性質(zhì)驗證算法的實現(xiàn) 50-51     5.3 資源驗證模塊的設(shè)計與實現(xiàn) 51-55         5.3.1 資源驗證模塊輸入接口設(shè)計 51-53       &

13、#160; 5.3.2 資源接口自動機組合模型的建立 53         5.3.3 資源驗證算法的實現(xiàn) 53-55     5.4 能耗驗證模塊的設(shè)計與實現(xiàn) 55-57         5.4.1 能耗驗證模塊輸入接口設(shè)計 55-56         5.4.2 能耗接口自動機組合模型的建立 56     

14、0;   5.4.3 能耗驗證算法的實現(xiàn) 56-57     5.5 本章小結(jié) 57-58 第六章 T-CBESD的測試以及應(yīng)用 58-69     6.1 測試 58-59     6.2 實例應(yīng)用 59-68         6.2.1 火災(zāi)預(yù)警組合系統(tǒng)實例應(yīng)用 59-64         6.2.2 通信構(gòu)件組合系統(tǒng)實例應(yīng)用 64-68 &#

15、160;   6.3 小結(jié) 68-69 第七章 總結(jié)和展望 69-71     7.1 總結(jié) 69-70     7.2 展望 70-71 參考文獻(xiàn) 71-75     4.2 T-CBESD開發(fā)及運行環(huán)境 36     4.3 T-CBESD體系結(jié)構(gòu)以及界面設(shè)計 36-40         4.3.1 T-CBESD體系結(jié)構(gòu) 36-38     

16、    4.3.2 T-CBESD界面設(shè)計 38-40     4.4 功能驗證模塊的設(shè)計與實現(xiàn) 40-46         4.4.1 功能驗證模塊的設(shè)計 40-41         4.4.2 功能驗證模塊輸入輸出接口的設(shè)計實現(xiàn) 41-42         4.4.3 UML 順序圖模型的輸入預(yù)處理 42-43  

17、       4.4.4 基本接口自動機組合模型的建立 43-44         4.4.5 非實時功能行為驗證算法的實現(xiàn) 44-46     4.5 本章小結(jié) 46-47 第五章 T-CBESD非功能性質(zhì)驗證模塊的設(shè)計與實現(xiàn) 47-58     5.1 非功能性質(zhì)驗證模塊的設(shè)計 47-48     5.2 實時驗證模塊的設(shè)計與實現(xiàn) 48-51   

18、60;     5.2.1 實時驗證模塊輸入輸出接口設(shè)計 48-49         5.2.2 帶時間約束的UML 順序圖的輸入預(yù)處理 49-50         5.2.3 實時接口自動機組合模型的建立 50         5.2.4 實時功能性質(zhì)驗證算法的實現(xiàn) 50-51     5.3 資源驗證模塊的設(shè)計與實

19、現(xiàn) 51-55         5.3.1 資源驗證模塊輸入接口設(shè)計 51-53         5.3.2 資源接口自動機組合模型的建立 53         5.3.3 資源驗證算法的實現(xiàn) 53-55     5.4 能耗驗證模塊的設(shè)計與實現(xiàn) 55-57         5.4.1 能

20、耗驗證模塊輸入接口設(shè)計 55-56         5.4.2 能耗接口自動機組合模型的建立 56         5.4.3 能耗驗證算法的實現(xiàn) 56-57     5.5 本章小結(jié) 57-58 第六章 T-CBESD的測試以及應(yīng)用 58-69     6.1 測試 58-59     6.2 實例應(yīng)用 59-68     &

21、#160;   6.2.1 火災(zāi)預(yù)警組合系統(tǒng)實例應(yīng)用 59-64         6.2.2 通信構(gòu)件組合系統(tǒng)實例應(yīng)用 64-68     6.3 小結(jié) 68-69 第七章 總結(jié)和展望 69-71     7.1 總結(jié) 69-70     7.2 展望 70-71 參考文獻(xiàn) 71-75     4.2 T-CBESD開發(fā)及運行環(huán)境 36     4.3 T-

22、CBESD體系結(jié)構(gòu)以及界面設(shè)計 36-40         4.3.1 T-CBESD體系結(jié)構(gòu) 36-38         4.3.2 T-CBESD界面設(shè)計 38-40     4.4 功能驗證模塊的設(shè)計與實現(xiàn) 40-46         4.4.1 功能驗證模塊的設(shè)計 40-41       &

23、#160; 4.4.2 功能驗證模塊輸入輸出接口的設(shè)計實現(xiàn) 41-42         4.4.3 UML 順序圖模型的輸入預(yù)處理 42-43         4.4.4 基本接口自動機組合模型的建立 43-44         4.4.5 非實時功能行為驗證算法的實現(xiàn) 44-46     4.5 本章小結(jié) 46-47 第五章 T-CBESD非功能性質(zhì)驗證模

24、塊的設(shè)計與實現(xiàn) 47-58     5.1 非功能性質(zhì)驗證模塊的設(shè)計 47-48     5.2 實時驗證模塊的設(shè)計與實現(xiàn) 48-51         5.2.1 實時驗證模塊輸入輸出接口設(shè)計 48-49         5.2.2 帶時間約束的UML 順序圖的輸入預(yù)處理 49-50         5.2.3 實時接口自動機組合模型的建立 50         5.2.4 實時功能性質(zhì)驗證算法的實現(xiàn) 50-51     5.3 資源驗證模塊的設(shè)計與實現(xiàn) 51-55