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

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

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

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