基于SPIN的UML模型一致性驗(yàn)證的研究及應(yīng)用.pdf

1、隨著計(jì)算機(jī)技術(shù)的高速發(fā)展，軟件系統(tǒng)的復(fù)雜性和規(guī)模也越來越高，為了解決大型軟件系統(tǒng)的設(shè)計(jì)和開發(fā)問題，UML提供了多種面向?qū)ο蠓治龊驮O(shè)計(jì)的建模視圖，支持對(duì)各種復(fù)雜系統(tǒng)進(jìn)行可視化分析、設(shè)計(jì)和軟件部署。然而，由于UML缺乏精確的形式化描述和語義定義，使得各種視圖之間很難保證模型的一致性和正確性。近年來，模型的一致性和正確性檢測(cè)成為一個(gè)非常突出和重要的研究課題，但目前的大多數(shù)研究方法是通過人工審查或形式化推理等半自動(dòng)的方式進(jìn)行檢測(cè)，不適合工業(yè)化應(yīng)

2、用。模型檢測(cè)技術(shù)是一種快速、全自動(dòng)的形式化驗(yàn)證方法，本文針對(duì)UML模型之間存在語義重疊和信息冗余等問題，結(jié)合SPIN檢測(cè)工具對(duì)UML模型進(jìn)行正確性和一致性驗(yàn)證，本文所做的工作如下：
　　首先，綜合分析了UML類圖、活動(dòng)圖和時(shí)序圖的元素，采用嚴(yán)格的形式化對(duì)其語法和語義進(jìn)行描述；由于對(duì)UML模型執(zhí)行一致性檢測(cè)須保證模型本身的正確性，同時(shí)對(duì)帶有嵌套結(jié)構(gòu)的多層次活動(dòng)圖難以解析其模型元素和不易實(shí)現(xiàn)自動(dòng)化驗(yàn)證，因此提出以樹形結(jié)構(gòu)對(duì)多層次活動(dòng)圖

3、進(jìn)行分解，并對(duì)分解完成的簡(jiǎn)單子圖進(jìn)行標(biāo)準(zhǔn)化和完整性檢測(cè)；繼而提出 UML活動(dòng)圖到Promela模型的轉(zhuǎn)換規(guī)則和Promela模型的重組算法，從而實(shí)現(xiàn)了多層次活動(dòng)圖活性及可靠性的驗(yàn)證。
　　接著，針對(duì)類圖、時(shí)序圖與活動(dòng)圖之間的一致性問題，定義了時(shí)序圖消息的順序關(guān)系以及UML模型之間的一致性語義，基于消息的順序關(guān)系對(duì)時(shí)序圖消息進(jìn)行約簡(jiǎn)，從而實(shí)現(xiàn)了時(shí)序圖對(duì)象的交互行為到活動(dòng)圖控制軌跡的轉(zhuǎn)換；繼而通過詳細(xì)分析 SPIN的驗(yàn)證機(jī)制，提出基于