嵌入式軟件可信性建模與驗證技術(shù)的研究及其應(yīng)用.pdf

1、嵌入式軟件在關(guān)鍵領(lǐng)域的廣泛應(yīng)用使其對可信性的需求遠遠高于一般軟件。由于嵌入式軟件在體系架構(gòu)、資源限制、應(yīng)用環(huán)境等方面的特殊性，以及近年來復(fù)雜化、規(guī)?；c開放化的發(fā)展趨勢，保障和評估嵌入式軟件的可信性已成為國內(nèi)外越來越關(guān)注的研究熱點之一。在嵌入式軟件開發(fā)早期對其可信性進行分析、驗證與評估，能夠減少潛在的軟件缺陷，從而降低后期測試與維護的成本。
　　本文立足于可信嵌入式軟件的建模與驗證問題，旨在建立基于模型驅(qū)動的嵌入式軟件建模與驗證集

2、成框架；采用Z語言為該框架提供形式化語義，針對嵌入式軟件可信屬性開展建模、驗證與評估技術(shù)的研究；設(shè)計并實現(xiàn)了相應(yīng)的原型系統(tǒng)，在嵌入式軟件實例上進行應(yīng)用研究。論文研究工作的主要創(chuàng)新性成果如下：
　?。?）根據(jù)嵌入式軟件的可信需求，提出了一種嵌入式軟件形式化模型Z-MARTE，包括Z-MARTE時間模型、結(jié)構(gòu)模型與行為模型。與現(xiàn)有模型相比，Z-MARTE是一種靜態(tài)結(jié)構(gòu)與動態(tài)行為的綜合模型，能夠同時描述嵌入式軟件功能結(jié)構(gòu)、時序行為以及可

3、信約束。在Z-MARTE模型中引入了可信構(gòu)造型的概念，通過對可信構(gòu)造型的聲明與約束，能夠描述包括數(shù)據(jù)約束與時間約束在內(nèi)的各類可信約束，為嵌入式軟件可信性的驗證與評估提供形式化語義基礎(chǔ)。
　?。?）為了對Z-MARTE模型描述的可信約束進行自動驗證，提出了一種基于模型檢測技術(shù)的嵌入式軟件可信驗證方法。首先，給出了有限域上Z-MARTE行為模型的語義解釋，為模型檢測方法提供了行為語義基礎(chǔ)；其次，擴展了CTL的語法與語義，定義了一種描述

4、嵌入式軟件可信性質(zhì)的時序邏輯公式ZMTL；最后，設(shè)計了有限域Z-MARTE行為模型上的模型檢測算法FZMCA，能夠在有限域內(nèi)對Z-MARTE模型中的實時性、安全性等可信性質(zhì)進行自動驗證。
　?。?）為了對Z-MARTE模型進行進一步的評估與分析，提出了一種嵌入式軟件風險評估方法RAMES。首先，對Z-MARTE結(jié)構(gòu)模型進行精化與擴展，提出了一種嵌入式軟件對象-消息-角色模型OMR；在此基礎(chǔ)上提出了風險分析算法RAOMR，以O(shè)MR模

5、型中的嵌入式軟件對象為評估單位，以對象間的通信行為與軟件安全約束為評估依據(jù)進行風險評估，并進行了算法復(fù)雜度分析與實例研究。RAMES方法遵循ISO31000標準的風險管理過程，其評估結(jié)果能夠指導(dǎo)嵌入式軟件設(shè)計模型中安全資源的合理分配。
　?。?）在上述研究成果的基礎(chǔ)上，建立了一個嵌入式軟件可信性建模與驗證集成框架，設(shè)計并初步實現(xiàn)了一個原型系統(tǒng)。在Eclipse平臺上初步實現(xiàn)了一個基于XSLT轉(zhuǎn)換技術(shù)的模型轉(zhuǎn)換工具ZMT，將半形式化