基于Petri網(wǎng)的UML狀態(tài)圖的形式化驗(yàn)證.pdf

1、統(tǒng)一建模語(yǔ)言(UML，Unified Modeling Language)是一種非專利的可視化建模和規(guī)約語(yǔ)言。UML提供了開放的方法，用于系統(tǒng)說明、文檔化、可視化構(gòu)建面向?qū)ο蟮能浖芗到y(tǒng)。然而UML并沒有被賦予嚴(yán)格的形式化語(yǔ)義，而且對(duì)于動(dòng)態(tài)模型僅僅只能描述而無法執(zhí)行，這使得模型的驗(yàn)證成為一個(gè)難題。造成軟件系統(tǒng)的許多缺陷在軟件設(shè)計(jì)開發(fā)初期很難發(fā)現(xiàn)，導(dǎo)致開發(fā)成本的增加。相對(duì)而言，Petri網(wǎng)擁有豐富的理論基礎(chǔ)，嚴(yán)格的形式化語(yǔ)義，而且是一種

2、可執(zhí)行的模型。本文著眼于兩種模型的優(yōu)勢(shì)，將UML模型中的狀態(tài)圖轉(zhuǎn)換為Petri網(wǎng)模型，進(jìn)而通過對(duì)Petri網(wǎng)模型的分析驗(yàn)證達(dá)到確保原模型正確性和合理性的目的。
　　 本文首先針對(duì)UML和Petri網(wǎng)兩種模型映射的國(guó)內(nèi)外研究現(xiàn)狀進(jìn)行了分析和綜述，基于相關(guān)的Petri網(wǎng)基礎(chǔ)理論，在研究UML狀態(tài)圖向Petri網(wǎng)映射的方法中，以圖模型為基礎(chǔ)，提出了具體的映射規(guī)則，然后對(duì)映射規(guī)則的正確性進(jìn)行了形式化證明，以確保二者語(yǔ)義上的等價(jià)性。在完成

3、兩種模型的映射基礎(chǔ)上，設(shè)計(jì)開發(fā)了二者的自動(dòng)轉(zhuǎn)換工具，并通過一個(gè)實(shí)例討論和分析了轉(zhuǎn)換工具的工作流程合理性。
　　 本文以設(shè)計(jì)一個(gè)小型網(wǎng)絡(luò)購(gòu)物系統(tǒng)為實(shí)例，首先基于VP-UML設(shè)計(jì)系統(tǒng)的用例圖、類圖以及訂單對(duì)象的狀態(tài)圖;然后針對(duì)訂單對(duì)象狀態(tài)圖，采用本文所提出的方法，使用自動(dòng)轉(zhuǎn)換工具將其轉(zhuǎn)為Petri網(wǎng)模型;最后根據(jù)Petri網(wǎng)理論對(duì)該模型進(jìn)行相關(guān)的性質(zhì)分析和行為驗(yàn)證。通過實(shí)例驗(yàn)證了映射方法的可行性和正確性。
　　 本文的主要工