基于SBOPN的UML模型的正確性驗(yàn)證.pdf

1、作為面向?qū)ο蠹夹g(shù)的標(biāo)準(zhǔn)語(yǔ)言,UML具有界面友好、易于表達(dá)、功能強(qiáng)大且普遍適用的特征,但是UML不是形式化的建模語(yǔ)言,缺乏精確的語(yǔ)義描述,因此難以在UML模型設(shè)計(jì)的早期階段對(duì)模型進(jìn)行分析驗(yàn)證.作為一種建模工具,Petri網(wǎng)既能對(duì)分布、并發(fā)的過(guò)程進(jìn)行有效的形式化建模,又能對(duì)系統(tǒng)的結(jié)構(gòu)和動(dòng)態(tài)行為進(jìn)行嚴(yán)密的數(shù)學(xué)分析和直觀的計(jì)算機(jī)仿真,因此我們選擇Petri網(wǎng)作為UML形式化方法.本文介紹了基于狀態(tài)的對(duì)象Petri網(wǎng)(State-Based Ob

2、ject Petri Net,SBOPN),給出網(wǎng)的定義、引發(fā)規(guī)則和網(wǎng)的分析方法,并討論其面向?qū)ο蟮奶卣?在此基礎(chǔ)上我們利用基于狀態(tài)的對(duì)象Petri網(wǎng)對(duì)UML進(jìn)行形式化,給出UML模型中的狀態(tài)圖和協(xié)作圖映射為基于狀態(tài)的對(duì)象Petri網(wǎng)模型的機(jī)制和相應(yīng)的實(shí)現(xiàn)算法,通過(guò)這些算法生成的Petri網(wǎng)模型既擁有其面向?qū)ο蟮奶卣?又可以利用Petri網(wǎng)的強(qiáng)大的分析工具對(duì)模型的進(jìn)行分析驗(yàn)證,找出死鎖狀態(tài),從而可以在模型設(shè)計(jì)的早期階段實(shí)現(xiàn)對(duì)模型的正確性