基于Petri網(wǎng)的形式化軟件開發(fā)方法研究.pdf

1、隨著計算機軟件的飛速發(fā)展，提高軟件開發(fā)的效率已成為一個非常重要的問題。采用軟件形式化技術，不僅可以極大地減少軟件設計早期階段的錯誤，縮短開發(fā)的總體時間，而且有利于開發(fā)人員之間的溝通，提高軟件的可靠性。形式化方法是建立在嚴格數(shù)學基礎上，通過嚴格的分析、驗證發(fā)現(xiàn)軟件設計及開發(fā)過程中的模糊性和不完備性，以達到對軟件質(zhì)量、開發(fā)成本及開發(fā)進度的有效控制。形式化方法分為形式化規(guī)格說明和形式化驗證。Petri網(wǎng)是滿足上述兩個要求的很好的描述工具。

2、 Petri網(wǎng)是一種對系統(tǒng)軟件形式化、圖形化的描述和分析工具，具有直觀、易懂和易用的優(yōu)點。對于具有并發(fā)、異步、分布、并行、不確定性和隨機性的系統(tǒng)，都可以利用這種工具構建模型。然后對模型進行分析，即可得到有關系統(tǒng)靜態(tài)結(jié)構和動態(tài)行為方面的信息。根據(jù)這些信息可以對要開發(fā)的系統(tǒng)進行評價和改進。同時，Petri網(wǎng)為程序員與其他人員之間的溝通和交流提供了一個強有力的一個平臺環(huán)境，使得軟件開發(fā)的過程形式化。 本文討論的是基于Petri網(wǎng)的

3、形式化軟件開發(fā)方法。主要從模擬與驗證兩方面展開。利用不變技術、結(jié)構分析技術、分塊建模技術等，對Petri網(wǎng)的模擬能力以及主要行為特征進行較深入細致的研究，得到了一些新的結(jié)果。本文的主要貢獻有： (1)數(shù)據(jù)庫系統(tǒng)的并發(fā)控制一直都受到業(yè)內(nèi)人士的廣泛關注，它是衡量一個DBMS性能的重要指標之一。而S.不變作為Petri網(wǎng)的一個重要的驗證方法同樣也越來越受到人們的關注。經(jīng)典的S不變方法往往只用來對系統(tǒng)性質(zhì)的一種解釋和判定，或是對一些具體

4、的范例的性質(zhì)的一種定性、定量分析。本文使用增廣Petri網(wǎng)構建一個比較通用的帶封鎖機制的DBMS模型，給出了形式化軟件開發(fā)的一個范例。從整體上模擬了一個DBMS，并用S不變對模型進行驗證?！弈壳埃蠖鄶?shù)的軟件系統(tǒng)都是并發(fā)系統(tǒng)。Petri作為一個很好的形式化描述和分析工具，必須要能很好的描述和分析這類系統(tǒng)。路燈故障檢測系統(tǒng)就是一個典型的并發(fā)系統(tǒng)，系統(tǒng)信號在路燈故障檢測系統(tǒng)與路燈設備以及傳輸線路之間是并行傳輸?shù)?。本文使用帶禁?容許弧的自控