基于UML的軟件模型檢測方法研究.pdf

1、隨著軟件的廣泛應用，特別是軟件在尖端領域的應用，軟件的可靠性成為一個非常重要的問題。軟件的可靠性主要取決于軟件開發(fā)的方法與過程，同時，又取決于軟件系統(tǒng)的測試與驗證。UML是面向?qū)ο箝_發(fā)中一種可視化建模語言，已經(jīng)成為事實上面向?qū)ο蠼５臉藴?。雖然UML表達豐富，但UML不是一種形式化的建模語言，其圖形化的符號經(jīng)常缺乏精確的語義。而且，傳統(tǒng)的驗證方法包括測試、模擬和仿真，它們均不能保證完全的錯誤覆蓋。因此，對軟件的UML模型進行形式化并對其

2、進行形式化的驗證非常必要。
　　 本文首先提出了一種基于UML的軟件模型檢測方法，其主要步驟如下：
　　 (1)將軟件的UML模型轉(zhuǎn)換為非形式化的基于XML的系統(tǒng)模型；
　　 (2)從基于XML的系統(tǒng)模型中提取系統(tǒng)信息，對其進行形式化轉(zhuǎn)換，得到系統(tǒng)的形式化的CTLMC語義模型；
　　 (3)采用形式化驗證工具CTLMC對形式化后的系統(tǒng)模型進行形式化驗證；
　　 (4)如果該模型不滿足用戶需求，CT

3、LMC給出反例信息并將其以UML順序圖的形式顯示表示。
　　 接著，著重介紹了采用該方法進行模型檢測所必須的兩個轉(zhuǎn)換工具(UML模型的形式化轉(zhuǎn)換工具和反例信息的UML順序圖轉(zhuǎn)換工具)的設計及實現(xiàn)。
　　 然后，將本支所實現(xiàn)的這兩個轉(zhuǎn)換工具與本實驗室開發(fā)的符號模型檢測器"CTLMC"相結合，實現(xiàn)了一個基于UML的軟件模型檢測系統(tǒng)。
　　 最后，通過兩個實例對所實現(xiàn)的基于UML的軟件模型檢測系統(tǒng)進行驗證。
　　

4、 根據(jù)本文提出的基于UML的軟件模型檢測方法所實現(xiàn)的基于UML的軟件模型檢測系統(tǒng)能夠結合軟件的UML類圖、UML狀態(tài)圖和UML順序圖對軟件的UML類圖中單個類所對應的UML狀態(tài)圖中各個狀態(tài)之間的狀態(tài)遷移關系及其約束進行驗證。采用本文提出的基于UML的軟件模型檢測方法，驗證人員可以在對形式化方法知之甚少或一無所知的情況下，對軟件的UML模型進行完全形式化的驗證，而且，本文提出的基于UML的軟件模型檢測方法，可以在很大程度上降低軟件系統(tǒng)的