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

1、現(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è)計前期缺乏有效工具對系績設(shè)計的功能性質(zhì)以及非功能性質(zhì)進(jìn)行分析與驗證。
　　 本文以接口自動機及其擴(kuò)展模型作為構(gòu)件化嵌入式軟件的設(shè)計模

2、型,以UML順序圖描述基于場景的功能規(guī)約,對基于接口自動機及其擴(kuò)展模型的多個模型檢驗抽象算法進(jìn)行分析且設(shè)計相應(yīng)的算法實現(xiàn)框架。進(jìn)而在Eclipse平臺上設(shè)計并實現(xiàn)了一個基于接口自動機模型的構(gòu)件化嵌入式軟件設(shè)計的形式化驗證原型工具T-CBESD(Tool for Component-Based Embedded SoftwareDesign)。該工具直接使用UML順序圖模型作為系統(tǒng)規(guī)約,可以檢驗系統(tǒng)設(shè)計模型與場景規(guī)約之間多種行為一致性問題