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

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

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

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

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