基于Petri網(wǎng)的UML模型分析及其在鐵道信號(hào)系統(tǒng)中的應(yīng)用研究.pdf

1、隨著信息技術(shù)的快速發(fā)展，計(jì)算機(jī)應(yīng)用日益廣泛，軟件已滲透到國(guó)民經(jīng)濟(jì)和國(guó)防建設(shè)的各個(gè)領(lǐng)域。但是軟件的生產(chǎn)現(xiàn)狀和質(zhì)量常常存在缺陷。因此，如何提高軟件的質(zhì)量，尤其在一些安全關(guān)鍵應(yīng)用領(lǐng)域，保證軟件的可靠性和安全性已成為國(guó)內(nèi)外研究的熱點(diǎn)問題。軟件的可靠性不僅取決于軟件開發(fā)的方法和過(guò)程，也取決于軟件的測(cè)試和驗(yàn)證。統(tǒng)一建模語(yǔ)言UML已廣泛應(yīng)用于安全關(guān)鍵計(jì)算機(jī)系統(tǒng)的開發(fā)中。它是一種功能強(qiáng)大、面向?qū)ο蟮目梢暬到y(tǒng)分析建模語(yǔ)言。但UML是半形式化的，不能用數(shù)

2、學(xué)工具直接的表達(dá)和分析，而且對(duì)象之間約束規(guī)則的一致性和并發(fā)性很難被UML模型所描述，其系統(tǒng)的動(dòng)態(tài)行為特征也難于全面地用UML模型體現(xiàn)。Petri網(wǎng)是一種系統(tǒng)的數(shù)學(xué)和圖形的建模分析工具，它以圖形化的數(shù)學(xué)工具庫(kù)所、變遷來(lái)清楚地描述系統(tǒng)內(nèi)部的相互作用，它特別適合描述系統(tǒng)中進(jìn)程或者部件的順序、并發(fā)、沖突以及同步等關(guān)系。因此，本文提出了一種將“UML狀態(tài)圖模型轉(zhuǎn)換為Petri網(wǎng)模型的方法”，并基于該方法，初步實(shí)現(xiàn)了一個(gè)將UML狀態(tài)圖模型轉(zhuǎn)換為Pe

3、tri網(wǎng)模型的自動(dòng)轉(zhuǎn)換工具。論文主要工作包括以下幾點(diǎn)：
　　 (1)針對(duì)國(guó)內(nèi)外的研究現(xiàn)狀，對(duì)軟件系統(tǒng)的形式化建模、描述及驗(yàn)證方法的研究和應(yīng)用進(jìn)行了分析。
　　 (2)對(duì)UML狀態(tài)圖進(jìn)行了研究，給出了UML狀態(tài)圖的形式化定義，并用定義的形式化語(yǔ)言描述了狀態(tài)圖的相關(guān)性質(zhì)、基本狀態(tài)和復(fù)合狀態(tài)。
　　 (3)通過(guò)分析UML狀態(tài)圖的形式化定義和Petri網(wǎng)嚴(yán)格的形式化語(yǔ)義，研究了兩者語(yǔ)義之間的等價(jià)部分，提出了將UML狀態(tài)圖