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

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

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

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