基于NuSMV的AUML模型形式化驗證.pdf

1、多Agent系統(tǒng)(MultiAgentSystemMAS)是解決分布式復(fù)雜問題的一種重要手段，也是一種新的軟件開發(fā)模式。為了適應(yīng)多Agent系統(tǒng)的建模需要，B.Bauer等人在2000年提出了擴(kuò)展的統(tǒng)一建模語言AUML。AUML雖然表達(dá)能力豐富，但卻不是形式化的描述語言，其圖形化的符號缺乏精確的定義，這使得對AUML所建立的系統(tǒng)模型難以進(jìn)行形式化推理和驗證。為了保證MAS系統(tǒng)設(shè)計的正確性，對AUML模型形式化語義轉(zhuǎn)換并進(jìn)行驗證十分必要。

2、 本文主要選取了AUML2.0的順序圖和交互概覽圖作為研究對象。為了有效地對AUML順序圖和交互概覽圖進(jìn)行形式化驗證，本文為AUML順序圖和交互概覽圖定義了一種可用于數(shù)據(jù)保存和交換的文本格式語言AODL，將AUML圖形模型轉(zhuǎn)換為AODL描述的文本；接著定義了一系列AUML到NuSMV的語義轉(zhuǎn)換規(guī)則，并設(shè)計和實現(xiàn)了基于這些規(guī)則的轉(zhuǎn)換程序，該程序以AODL文本為輸入，以smv文件為輸出，實現(xiàn)語義轉(zhuǎn)換的自動化；最后本文用NuSMV檢測

3、器對轉(zhuǎn)換得到的smv文件進(jìn)行性質(zhì)驗證。通過兩個協(xié)議實例的實驗證明，本文定義的語義轉(zhuǎn)換規(guī)則是有效的，形式化驗證AUML2.0模型圖是可行且有效的。 本文的成果，不僅定義了一系列從AUML2.0到NuSMV語義的映射規(guī)則，實現(xiàn)了一個將AODL所描述的AUML圖模型轉(zhuǎn)換為NuSMV模型的轉(zhuǎn)換程序，并用NuSMV檢測了AUML模型的性質(zhì)，通過檢測有助于指導(dǎo)建模者建立更加精確的模型；而且定義了一種可以描述AUML順序圖和交互概覽圖的數(shù)據(jù)交