基于Petri網(wǎng)的軟件模型驗(yàn)證.pdf

1、隨著軟件在人們生活中起著越來(lái)越重要的作用，如何提高軟件的質(zhì)量，保證軟件的可靠性和安全性成為一個(gè)重要的問(wèn)題。在軟件設(shè)計(jì)領(lǐng)域，UML成為廣泛運(yùn)用的軟件建模工具，但是UML作為一種半形式化語(yǔ)言，缺乏精確的描述和形式化定義，很難驗(yàn)證模型的正確性。Petri網(wǎng)既是一種圖形化建模工具，又是具有嚴(yán)格的語(yǔ)法語(yǔ)義定義的形式化方法，不但能有效地對(duì)系統(tǒng)進(jìn)行描述和建模，對(duì)系統(tǒng)的并發(fā)性、異步性和不確定性也有很強(qiáng)的動(dòng)態(tài)分析能力。通過(guò)將UML模型轉(zhuǎn)化為Petri網(wǎng)模

2、型，再利用Petri網(wǎng)的分析驗(yàn)證技術(shù)，可以實(shí)現(xiàn)對(duì)軟件模型的正確性的驗(yàn)證，在設(shè)計(jì)階段即發(fā)現(xiàn)系統(tǒng)的缺陷，從而減少軟件開發(fā)后期才發(fā)現(xiàn)設(shè)計(jì)的錯(cuò)誤而帶來(lái)的損失，提高系統(tǒng)的正確性和安全性。 本文提出一種系統(tǒng)層次上的對(duì)UML狀態(tài)圖進(jìn)行驗(yàn)證的方法，將UML狀態(tài)圖轉(zhuǎn)換為系統(tǒng)層上的Petri網(wǎng)，然后使用模型檢測(cè)的方法驗(yàn)證UML狀態(tài)圖轉(zhuǎn)換得到的Petri網(wǎng)模型。并且通過(guò)驗(yàn)證狀態(tài)圖轉(zhuǎn)換得到的Petri網(wǎng)模型是否滿足協(xié)作圖描述的用例而驗(yàn)證協(xié)作圖，從而驗(yàn)證

3、系統(tǒng)的動(dòng)態(tài)行為。 本文通過(guò)將UML模型的XMI格式進(jìn)行解析，使用DOM API實(shí)現(xiàn)了UML模型向Petri網(wǎng)標(biāo)識(shí)語(yǔ)言PNML自動(dòng)轉(zhuǎn)換。PNML可以被Petri網(wǎng)建模工具CPNTools識(shí)別，從而對(duì)轉(zhuǎn)換得到的Petri網(wǎng)模型進(jìn)行分析和模型驗(yàn)證。CPN Tools提供了一個(gè)可視化的界面，可以對(duì)Petri網(wǎng)模型進(jìn)行編輯和仿真，同時(shí)也可以驗(yàn)證模型是否滿足ASK-CTL公式描述的性質(zhì)。 最后，本文通過(guò)實(shí)例測(cè)試了在Borland T