基于UML的軟件模型檢測方法研究與應(yīng)用.pdf

1、統(tǒng)一建模語言UML(United Modeling Language)是一種面向?qū)ο蠓治龊驮O(shè)計的可視化建模語言，其建模環(huán)境及其軟件開發(fā)過程已被各界廣泛認(rèn)可及應(yīng)用，但是其圖形化的語言缺乏精確的語義描述，加之當(dāng)前軟件系統(tǒng)的規(guī)模及自身的復(fù)雜性不斷增大，導(dǎo)致使用UML建模的軟件系統(tǒng)的正確性及有效性難以得到保證，而形式化方法可以很好地彌補(bǔ)UML在語義描述上的欠缺。因此，基于UML的軟件形式化驗證的研究具有很強(qiáng)的現(xiàn)實意義。模型檢測技術(shù)是當(dāng)前一種應(yīng)用

2、比較廣泛的形式化驗證方法，近來學(xué)術(shù)界努力地將其在硬件領(lǐng)域的成功延伸到軟件領(lǐng)域，以加快軟件系統(tǒng)形式化驗證的研究進(jìn)程。目前，基于模型檢測技術(shù)對軟件進(jìn)行形式化驗證的研究已成為熱點(diǎn)。
　　本文將軟件設(shè)計階段的UML模型的形式化驗證方法作為研究對象，在查閱大量資料、深入學(xué)習(xí)相關(guān)知識、總結(jié)國內(nèi)外在該領(lǐng)域的研究現(xiàn)狀及其成果的基礎(chǔ)上進(jìn)行了深入的研究，主要包括三個方面的工作：
　　首先，闡述了模型檢測工具SPIN的工作原理和特點(diǎn)，并深入學(xué)習(xí)了

3、其輸入語言Promela和線性時態(tài)邏輯公式LTL；
　　其次，制定了一套涵蓋UML模型靜態(tài)信息和動態(tài)行為的形式化轉(zhuǎn)換規(guī)則，同時實現(xiàn)了在SPIN的平臺下對一組包含類圖、狀態(tài)圖及協(xié)作圖的UML模型子集的形式化驗證；
　　最后，基于復(fù)雜多層次的狀態(tài)圖和UML2.0順序圖所增加的交互片段概念，改進(jìn)了一種UML模型視圖間動態(tài)特性的一致性驗證方法，在該方法中，嘗試使用基于XYZ/E的中間方法實現(xiàn)對狀態(tài)圖的形式化轉(zhuǎn)換，通過驗證狀態(tài)圖所對應(yīng)