形式化開發(fā)方法-Petri網(wǎng)

《形式化開發(fā)方法-Petri網(wǎng)》由會員上傳分享，免費在線閱讀，更多相關(guān)內(nèi)容在教育資源-天天文庫。

1、軟件工程形式化方法第5章形式化開發(fā)方法(1)內(nèi)容安排軟件開發(fā)的形式化方法形式化開發(fā)方法(1)–Petri網(wǎng)形式化開發(fā)方法(2)–時態(tài)邏輯形式化開發(fā)方法(3)–Z方法3軟件開發(fā)的形式化方法軟件開發(fā)的形式化方法定義軟件開發(fā)的形式化方法（formalmethods）是建立在嚴格數(shù)學基礎(chǔ)上，具有精確數(shù)學語義的開發(fā)方法簡單地說，凡在系統(tǒng)研究中，應(yīng)用了數(shù)學的方法，都是形式化方法本章所介紹的形式化開發(fā)方法是指軟件規(guī)格說明數(shù)學建模、數(shù)學驗證和數(shù)學程序求精4形式化方法與結(jié)構(gòu)化和OO方法區(qū)別結(jié)構(gòu)化和OO方法使用了大量的自然語言。自然語言的二義

2、性、不完整和抽象層次的混雜等問題的解決，必然使開發(fā)系統(tǒng)的質(zhì)量不高、成本增加和進度拖長；尤其對安全性或其他質(zhì)量因素要求極高的軟件，任何微小的錯誤都可能帶來災難性的后果形式化的方法可以幫助軟件開發(fā)人員開發(fā)出更為無二義性、完整的和準確的需求規(guī)格說明，進而通過嚴格的驗證發(fā)現(xiàn)問題，以達到對軟件質(zhì)量、開發(fā)成本和開發(fā)進度的有效控制5形式化開發(fā)方法發(fā)展歷史20世紀60年代末形式化方法與非形式化大致同步都是為解決當時出現(xiàn)的“軟件危機”提出一般認為是Floyd、Hoare和Manna等在程序正確性證明方面的研究。但由于這些方法受程序規(guī)模的限制

3、而未能應(yīng)用20世紀80年代末在硬件設(shè)計領(lǐng)域形式化方法的工業(yè)應(yīng)用結(jié)果，又掀起了軟件形式化開發(fā)方法的學術(shù)研究和工業(yè)應(yīng)用的熱潮，建立了一些較為成熟的方法和語言如Petri網(wǎng)、statecharts、通信順序過程、通信系統(tǒng)演算、程序正確性證明、時態(tài)邏輯、模型驗證、Z語言、VDM及Larch等6目前流行的形式化開發(fā)方法形式化規(guī)格說明建模形式化驗證形式化程序求精7形式化規(guī)格說明建模操作類基于狀態(tài)和轉(zhuǎn)移Petri網(wǎng)、有限狀態(tài)機和狀態(tài)圖描述類基于數(shù)學公理和概念基于邏輯的描述方法：命題線性時態(tài)邏輯（PLTL）、一階線性時態(tài)邏輯（FOLTL）

4、、計算樹邏輯（CTL）基于代數(shù)的描述方法：Z語言、VDM和Larch雙重類兼有操作類和描述類兩者的特點擴展狀態(tài)機（ESM）、實時時態(tài)邏輯（RTTL）8形式化驗證模型驗證和定理證明模型驗證是對規(guī)格說明所建立起來的模型狀態(tài)空間進行搜索，以確認該系統(tǒng)模型是否具有所期望的某些性質(zhì)定理證明是以邏輯公式作為系統(tǒng)及其性能的規(guī)格說明，其中邏輯由一個具有公理和推理規(guī)則的形式化系統(tǒng)給出。進行定理證明的過程就是應(yīng)用這些公理或推理規(guī)則來證明系統(tǒng)是否具有所期望的性質(zhì)9形式化程序求精形式化程序求精就是將自動推理與形式化規(guī)格說明相結(jié)合而形成的一門技術(shù)研

5、究如何從形式化的規(guī)格說明推演出具體的面向計算機的程序代碼的全過程基本思想就是用一個抽象程度低和過程性強的程序，去代替一個抽象程度高和過程性弱的程序，并保證它們的功能和性質(zhì)完全一致形式化程序求精與形式化規(guī)格說明和形式化驗證三者是緊密聯(lián)系和相輔相成10形式化開發(fā)方法主要問題對軟件開發(fā)人員（包括管理人員和用戶）的數(shù)學素質(zhì)有較高的要求主要是離散數(shù)學中的集合、代數(shù)結(jié)構(gòu)、數(shù)理邏輯等基礎(chǔ)內(nèi)容在軟件工程中的具體應(yīng)用對于原來一些數(shù)學背景較差的工程人員要花許多時間去學習和掌握。有的甚至還要克服對數(shù)學的畏懼心理在選擇和應(yīng)用形式化開發(fā)方法時應(yīng)注意

6、的問題Bowan和Hinchley提出了“形式化法方法的十條戒律”11形式化開發(fā)方法(1)Petri網(wǎng)12什么是Petri網(wǎng)Petri網(wǎng)是一種網(wǎng)狀結(jié)構(gòu)的系統(tǒng)的描述和分析工具對于具有并發(fā)、異步、分布、并行、不確定性或隨機性的信息系統(tǒng)，都可以利用這種工具構(gòu)造出要開發(fā)的Petri網(wǎng)模型。然后對其進行分析，即可得到有關(guān)系統(tǒng)結(jié)構(gòu)和動態(tài)行為方面的信息。根據(jù)這些信息就可以對要開發(fā)的系統(tǒng)進行評價和改進Petri網(wǎng)的提出由德國C.A.Petri在他的62年博士論文“Communicationwithautomata”中提出當時引起一些歐美科

7、學家的重視。他們在引用這種網(wǎng)狀結(jié)構(gòu)模擬和分析并行系統(tǒng)中稱它為“PetriNets”。從此以后大家都稱它為Petri網(wǎng)13Petri網(wǎng)介紹的內(nèi)容示例-四季系統(tǒng)ΣPetri網(wǎng)的定義Petri網(wǎng)的基本原理-靜態(tài)結(jié)構(gòu)Petri網(wǎng)的基本原理-動態(tài)特征建模實例特性分析Petri網(wǎng)的特性分析方法改進Petri網(wǎng)及其應(yīng)用時間網(wǎng)和隨機網(wǎng)從Petri網(wǎng)到程序結(jié)構(gòu)的轉(zhuǎn)換14示例：四季系統(tǒng)Σ一年有四季，四季氣候的變化該Σ系統(tǒng)可以由圖形表示15系統(tǒng)Σ的Petri網(wǎng)圖形表示16系統(tǒng)Σ的Petri網(wǎng)數(shù)學表示Σ=（P，T；F，M0）P={p1,p2,p3

8、,p4}T={t1,t2,t3,t4}F={（p1,t1）,（t1,p2）,（p2,t2）,（t2,p3）,（p3,t3）,（t3,p4）,（p4,t4）,（t4,p1）}M0=（0,0,0,1）17Petri網(wǎng)描述系統(tǒng)Σ的特點從四季系統(tǒng)Σ中，可以看出這種利用事物的因果關(guān)系對系統(tǒng)進行網(wǎng)狀結(jié)構(gòu)的描述，有以