基于模型檢測的UML形式化驗證的研究.pdf

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

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