基于模型檢測的UML形式化驗(yàn)證的研究.pdf

1、UML作為一種軟件面向?qū)ο蠓治龊驮O(shè)計(jì)的建模語言，已經(jīng)得到了廣泛的應(yīng)用，但是，在軟件的設(shè)計(jì)過程中，難免會引入一些錯(cuò)誤。傳統(tǒng)的軟件測試方法是在軟件開發(fā)完成之后進(jìn)行的，而如果能夠在軟件開發(fā)早期對系統(tǒng)設(shè)計(jì)進(jìn)行形式化驗(yàn)證，這樣既能保證軟件的可靠性，還可以提高開發(fā)效率，節(jié)約開發(fā)成本。模型檢測技術(shù)是一種主流的形式化驗(yàn)證方法，目前已經(jīng)在硬件和協(xié)議驗(yàn)證方面取得了成功，利用模型檢測技術(shù)對軟件進(jìn)行形式化驗(yàn)證成為近年來研究的一個(gè)熱點(diǎn)。
　　本文針對如何利

2、用模型檢測技術(shù)對軟件設(shè)計(jì)階段的UML模型進(jìn)行形式化驗(yàn)證這一問題進(jìn)行了研究，在汲取前人的經(jīng)驗(yàn)和教訓(xùn)的基礎(chǔ)上，提出了一套形式化轉(zhuǎn)換規(guī)則，改進(jìn)了一種UML模型動態(tài)特性的一致性驗(yàn)證方法，主要包括三個(gè)方面的工作:
　　首先，闡述了模型檢測工具SPIN的工作原理和特點(diǎn)，分析了選取SPIN作為模型檢測工具的優(yōu)勢，并且對其輸入語言Promela和線性時(shí)態(tài)邏輯LTL進(jìn)行了深入的分析;
　　其次，選取了一個(gè)包括類圖、狀態(tài)圖和協(xié)作圖在內(nèi)的UML子