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

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

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