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

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

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

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

4、適合描述一些順序系統(tǒng)，但是它也有缺點(diǎn)，它不適合描述實(shí)時(shí)系統(tǒng)和并發(fā)系統(tǒng)。鑒于以上兩種方法各自的缺陷，我們考慮將T P N和B 方法結(jié)合在一起，用B 方法作為T(mén) P N 底層的形式化模型，這一點(diǎn)和眾多高級(jí)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)的動(dòng)態(tài)映射，描述T B 網(wǎng)的動(dòng)態(tài)

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