基于B語言與TPN集成的形式化方法.pdf

1、2 0 0 6 屆研究生碩士學(xué)位論文y 8 9 { 9 9 3學(xué)校代碼：1 0 2 6 9學(xué) 號：Y s 0 0 3 2 4 1 0 1 3纂黎裙熬是擎基于B 語言與T P N 集成的形式化方法院 系：焦。墾堂瞳讓簋扭丕專 業(yè)：立￡篡盟塑仕蘭理迨研究方向：絲式垡友選指導(dǎo)教師： 韭掛戊副熬攫碩士研究生： 姜莖雅2 0 0 6 年4 月完成1 仁東帥弛人學(xué)汁算機(jī)系壩．J 。學(xué)位論文摘要隨著人們對軟件系統(tǒng)的要求不斷地提高，形式化技術(shù)得到了充分

2、的發(fā)展。過去人們依賴于優(yōu)秀的軟件工程師來對軟件系統(tǒng)可靠性和安全性提供保證，而如今，人們可以使用已有的形式化技術(shù)，按照一定的步驟逐步來開發(fā)出滿足市場高要求的軟件系統(tǒng)。然而，目前的形式化技術(shù)還比較單一，它們只能滿足開發(fā)人員對軟件系統(tǒng)設(shè)計的某些方面，因此，這種滿足有一定局限性和限制。隨著研究人員對這些形式化技術(shù)的研究的深入，人們逐漸發(fā)現(xiàn)了這些技術(shù)和方法本身存在著固有的缺陷。于是，人們開始對形式化方法的集成這一研究思路的探討，己有的集成的例子，

3、如c s P 和B 方法進(jìn)行的集成，c s P 和z 語言進(jìn)行的集成。本文研究的對象的基礎(chǔ)有兩個，分別是時問P e 仃i 網(wǎng)( T P N ) 和B 方法。T P N 是一種圖形化的形式化技術(shù)，它主要應(yīng)用于實(shí)時系統(tǒng)，分布式系統(tǒng)或者并發(fā)系統(tǒng)，它建立在普通的P e t r i 網(wǎng)基礎(chǔ)之上，并加以時間約束，和普通P e t r i 網(wǎng)一樣，它缺乏數(shù)據(jù)建模能力和函數(shù)定義能力。B 方法是一種形式化方法，它包含了自己的形式規(guī)格說明語言和驗證系統(tǒng)，它

4、適合描述一些順序系統(tǒng)，但是它也有缺點(diǎn)，它不適合描述實(shí)時系統(tǒng)和并發(fā)系統(tǒng)。鑒于以上兩種方法各自的缺陷，我們考慮將T P N和B 方法結(jié)合在一起，用B 方法作為T P N 底層的形式化模型，這一點(diǎn)和眾多高級P e t r i 網(wǎng)有非常多的相似之出。將B 方法作為底層模型之后，將B 方法中的某些元素替換原有T P N 中的概念，從而建立T P N 和B 方法之間映射關(guān)系。這種關(guān)系是靜態(tài)的，我們還需要定義T B 網(wǎng)的動態(tài)映射，描述T B 網(wǎng)的動態(tài)

5、性質(zhì)。T B網(wǎng)是一種高級的P e t r i 網(wǎng)，需要搞清楚這種網(wǎng)的構(gòu)造方法，它的可達(dá)圖的構(gòu)造，它的活性的定義，本文對于這些問題都進(jìn)行了探討。另外，由于T B 網(wǎng)是一種集成的形式化方法，它應(yīng)該能夠描述實(shí)時系統(tǒng)，我們需要指出如何能夠證明構(gòu)造出來的系統(tǒng)能夠滿足時間約束。T B 網(wǎng)是一種集成的形式化方法，它能夠使用的領(lǐng)域應(yīng)該包括了T P N 和B 方法各自使用的領(lǐng)域，這是因為在集成的過程中，我們使用B 方法來解決T P N 不能夠描述數(shù)據(jù)類型