基于模型檢測(cè)的UML形式化驗(yàn)證及其系統(tǒng)實(shí)現(xiàn).pdf

1、UML是面向?qū)ο箝_(kāi)發(fā)中一種可視化建模語(yǔ)言，已經(jīng)成為事實(shí)上的面向?qū)ο蠼?biāo)準(zhǔn)。雖然表達(dá)豐富，但UML不是形式化的建模語(yǔ)言，其圖形化的符號(hào)經(jīng)常缺乏精確的語(yǔ)義，這使得對(duì)UML進(jìn)行形式化推理十分困難。為了保證系統(tǒng)設(shè)計(jì)的正確性，在系統(tǒng)開(kāi)發(fā)早期的時(shí)候發(fā)現(xiàn)可能存在的錯(cuò)誤，進(jìn)而降低系統(tǒng)開(kāi)發(fā)的風(fēng)險(xiǎn)，對(duì)UML模型進(jìn)行形式化驗(yàn)證很有必要?！　”疚倪x取了UML模型的一個(gè)包括類(lèi)圖、狀態(tài)圖、順序圖或協(xié)作圖的的子集，研究了UML模型子集的NuSMV形式化語(yǔ)義，定義

2、了UML語(yǔ)義向NuSMV語(yǔ)義轉(zhuǎn)換的一系列規(guī)則，使得可以對(duì)半形式化的UML模型進(jìn)行NuSMV形式化轉(zhuǎn)換，并在此基礎(chǔ)上加以形式化驗(yàn)證，對(duì)于形式化驗(yàn)證，本文采用了模型檢測(cè)的方法。對(duì)NuSMV形式化驗(yàn)證的結(jié)果，本文進(jìn)行了分析，并且討論了如何將之轉(zhuǎn)換為UML模型的逆向工程的方法，對(duì)此同樣定義了將結(jié)果逆向工程到UML的一系列規(guī)則，使得能夠?qū)ML的形式化驗(yàn)證結(jié)果逆向轉(zhuǎn)換為UML模型。本文還進(jìn)一步設(shè)計(jì)并實(shí)現(xiàn)了基于上面轉(zhuǎn)換規(guī)則的UML向NuSMV語(yǔ)義轉(zhuǎn)

3、換以及從NuSMV逆向到UML模型的轉(zhuǎn)換工具，并將這兩個(gè)方向的轉(zhuǎn)換以及NuSMV模型檢測(cè)工具整合在一個(gè)系統(tǒng)中，實(shí)現(xiàn)了對(duì)UML的自動(dòng)形式化驗(yàn)證?！　∥覀?cè)贐orlandTogether等環(huán)境中測(cè)試和驗(yàn)證本文定義的規(guī)則和實(shí)現(xiàn)的系統(tǒng)的正確性，分別建立兩個(gè)不同應(yīng)用領(lǐng)域的UML模型，利用我們實(shí)現(xiàn)的系統(tǒng)對(duì)兩個(gè)實(shí)例進(jìn)行NuSMV轉(zhuǎn)換，并對(duì)NuSMV驗(yàn)證的結(jié)果逆向轉(zhuǎn)換為UML模型，從而實(shí)現(xiàn)了對(duì)于給定實(shí)例的自動(dòng)化驗(yàn)證。實(shí)際的測(cè)試與驗(yàn)證說(shuō)明了該系統(tǒng)能夠運(yùn)