基于SPIN的UML活動(dòng)圖驗(yàn)證.pdf

1、隨著計(jì)算機(jī)技術(shù)的飛速發(fā)展，軟件系統(tǒng)的廣泛應(yīng)用，軟件系統(tǒng)間的可移植性、協(xié)同工作能力和可維護(hù)性問(wèn)題日益突出，以模型為軟件開(kāi)發(fā)關(guān)鍵的模型驅(qū)動(dòng)架構(gòu)MDA方法是解決這些問(wèn)題而產(chǎn)生的新技術(shù)。用UML活動(dòng)圖建立MDA中的平臺(tái)無(wú)關(guān)模型PIM是模型的核心之一。但是很多模型在建模過(guò)程中缺乏正確性驗(yàn)證或僅進(jìn)行局部的語(yǔ)法檢驗(yàn)，造成模型存在死鎖、活鎖等缺陷，這直接引發(fā)了模型執(zhí)行過(guò)程中的諸多問(wèn)題，如任務(wù)不能完成、超期完成等。因而，在建模階段驗(yàn)證模型的正確性就顯得尤

2、為重要。模型檢測(cè)作為形式化驗(yàn)證模型的方法，有著自動(dòng)化和提供反例等諸多優(yōu)點(diǎn)。并且近年在UML模型中得到廣泛應(yīng)用。模型檢測(cè)器SPIN是由貝爾實(shí)驗(yàn)室開(kāi)發(fā)的一種專(zhuān)門(mén)用于軟件驗(yàn)證的工具。 本文基于模型檢測(cè)工具SPIN，對(duì)UML活動(dòng)圖建立的PIM模型進(jìn)行形式化分析和驗(yàn)證，并對(duì)UML活動(dòng)圖進(jìn)行動(dòng)態(tài)模擬。首先在UML活動(dòng)圖建立的PIM模型基礎(chǔ)上，將UML活動(dòng)圖轉(zhuǎn)化為模型驗(yàn)證工具SPIN能夠識(shí)別的PROMELA語(yǔ)言模型，然后結(jié)合SPIN的驗(yàn)證功能