第四章形式化說明技術(shù)

1、第四章形式化說明技術(shù) 軟件工程軟件工程 第四章 形式化說明技術(shù) 第四章形式化說明技術(shù) 第第4章章 形式化說明技術(shù)形式化說明技術(shù) 4 . 1 概述 4 . 2 例子 4 . 3 Petri 網(wǎng) 4 . 4 Z語言 4 . 5 小結(jié) 習(xí)題 第四章形式化說明技術(shù) 學(xué)習(xí)要求學(xué)習(xí)要求 掌握： 1：掌握形式化方法的概念、優(yōu)點(diǎn)和應(yīng)用準(zhǔn)則 2：初步掌握有窮狀態(tài)機(jī)、Petri網(wǎng)、Z語言的 概念和使用 理解： 第四章形式化說明技術(shù) 重點(diǎn)和難點(diǎn)重點(diǎn)和難點(diǎn) 重點(diǎn): 1：形式化方法的概念、優(yōu)點(diǎn)和應(yīng)用準(zhǔn)則 2：有窮狀態(tài)機(jī) 難點(diǎn): 1：有窮狀態(tài)機(jī) 2：Petri網(wǎng)形式化方法的優(yōu)點(diǎn)和適用情況 第四章形式化說明技術(shù) 所謂形式化

2、方法：是描述系統(tǒng)性質(zhì)的，是基 于數(shù)學(xué)的技術(shù)，也就是說，如果一種方法有 堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)，那么它就是形式化的。 第四章形式化說明技術(shù) 4.1概述概述 5.2.1模塊化 5.2.2抽象 5.2.3逐步求精 5.2.4信息隱蔽和局部化 5.2.4模塊獨(dú)立 4. 1 .1 非形式化方法缺點(diǎn)非形式化方法缺點(diǎn) 用自然語言書寫的系統(tǒng)規(guī)格說明書，可能存 在矛盾、二義性、含糊性、不完整性及抽象層 次混亂等問題。 第四章形式化說明技術(shù) 4. 1 .2 形式化方法優(yōu)點(diǎn)形式化方法優(yōu)點(diǎn) 在軟件開發(fā)中引入數(shù)學(xué)，創(chuàng)造基于數(shù)學(xué)的形 式化方法。具體介紹形式化方法的優(yōu)點(diǎn)： 1：能夠簡(jiǎn)潔準(zhǔn)確地描述物理現(xiàn)象、對(duì)象或動(dòng) 作的結(jié)果，因此是

3、理想的建模工具。 2：可以在不同的軟件活動(dòng)之間平滑地過渡。 3：提供了高層確認(rèn)的手段。 第四章形式化說明技術(shù) 4. 1 .3 應(yīng)用形式化方法的準(zhǔn)則應(yīng)用形式化方法的準(zhǔn)則 1：選用適當(dāng)?shù)谋硎痉椒ā?2：應(yīng)該形式化，但不要過分形式化。 3：應(yīng)該估算成本。 4：應(yīng)該有形式化方法顧問隨時(shí)提供咨詢。 5：不應(yīng)該放棄傳統(tǒng)的開發(fā)方法。 6：應(yīng)該建立詳盡的文檔。 7：不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)。 第四章形式化說明技術(shù) 4. 1 .3 應(yīng)用形式化方法的準(zhǔn)則應(yīng)用形式化方法的準(zhǔn)則 8：不應(yīng)該盲目依賴形式化方法。 9：應(yīng)該測(cè)試、測(cè)試再測(cè)試。 10：應(yīng)該重用。 第四章形式化說明技術(shù) 4 . 2 有窮狀態(tài)機(jī)有窮狀態(tài)機(jī) 引入狀態(tài)機(jī)的

4、概有窮狀態(tài)機(jī)的概念念 4. 2 .1 有窮狀態(tài)機(jī)概念有窮狀態(tài)機(jī)概念 引入一個(gè)簡(jiǎn)單的例子。引入一個(gè)簡(jiǎn)單的例子。 一個(gè)保險(xiǎn)箱上裝了一個(gè)復(fù)合鎖，鎖有三個(gè)位一個(gè)保險(xiǎn)箱上裝了一個(gè)復(fù)合鎖，鎖有三個(gè)位 置，分別標(biāo)記為置，分別標(biāo)記為1、2、3，轉(zhuǎn)盤可向左（，轉(zhuǎn)盤可向左（L） 或向右（或向右（R）轉(zhuǎn)動(dòng)。這樣，在任意時(shí)刻轉(zhuǎn)盤都）轉(zhuǎn)動(dòng)。這樣，在任意時(shí)刻轉(zhuǎn)盤都 有有6種可能的運(yùn)動(dòng)，即種可能的運(yùn)動(dòng)，即1L、1R、2L、2R、3L、 3R。保險(xiǎn)箱的組合密碼是。保險(xiǎn)箱的組合密碼是1L、3R、2L，轉(zhuǎn)，轉(zhuǎn) 盤的任何其他運(yùn)動(dòng)都將引起報(bào)警。具體見盤的任何其他運(yùn)動(dòng)都將引起報(bào)警。具體見圖圖 4.1保險(xiǎn)箱的狀態(tài)轉(zhuǎn)換圖保險(xiǎn)箱的狀態(tài)轉(zhuǎn)換圖

5、 第四章形式化說明技術(shù) 4.2.1有窮狀態(tài)機(jī)的概有窮狀態(tài)機(jī)的概念念 圖4.1保險(xiǎn)箱的狀態(tài)轉(zhuǎn)換圖 第四章形式化說明技術(shù) 4.2.1有窮狀態(tài)機(jī)的概有窮狀態(tài)機(jī)的概念念 第四章形式化說明技術(shù) 4.2.1有窮狀態(tài)機(jī)的概有窮狀態(tài)機(jī)的概念念 從上述 個(gè)的例子可以看出： 一個(gè)有窮狀態(tài)機(jī)包括下述5個(gè)部分：狀態(tài)集J、 輸入集K、由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個(gè) 狀態(tài)（次態(tài)）的轉(zhuǎn)換函數(shù)T、初始態(tài)S和終態(tài) 集F。 第四章形式化說明技術(shù) 4.2.1有窮狀態(tài)機(jī)的概有窮狀態(tài)機(jī)的概念念 對(duì)于保險(xiǎn)箱的例子，相應(yīng)的有窮狀態(tài)機(jī)的各 部分如下： 狀態(tài)集J：保險(xiǎn)箱鎖定，A，B，保險(xiǎn)箱解鎖， 報(bào)警 輸入集K：1L、1R、2L、2R、3L、

6、3R 轉(zhuǎn)換函數(shù)T：如表4.1所示 初始態(tài)S：保險(xiǎn)箱鎖定 終態(tài)集F：保險(xiǎn)箱解鎖，報(bào)警 第四章形式化說明技術(shù) 4.2.1有窮狀態(tài)機(jī)的概有窮狀態(tài)機(jī)的概念念 如果使用更形式化的術(shù)語，一個(gè)有窮狀態(tài)機(jī) 可以表示為一個(gè)5元組(J,K,T,S,F)，其中： J是一個(gè)有窮的非空狀態(tài)集； K是一個(gè)有窮的非空輸入集； T是一個(gè)從(J-F)K到J的轉(zhuǎn)換函數(shù)； SJ，是一個(gè)初始狀態(tài)； F J，是終態(tài)集。 第四章形式化說明技術(shù) 4.2.1有窮狀態(tài)機(jī)的概有窮狀態(tài)機(jī)的概念念 為了對(duì)一個(gè)系統(tǒng)進(jìn)行規(guī)格說明，通常都需要 對(duì)有窮狀態(tài)機(jī)做一個(gè)很有用的擴(kuò)展，即在前 述的5元組中加入第6個(gè)組件謂詞集P，從而 把有窮狀態(tài)機(jī)擴(kuò)展為一個(gè)6元祖，

7、其中的每個(gè) 謂詞都是系統(tǒng)全局狀態(tài)Y的函數(shù)。轉(zhuǎn)換函數(shù)T 現(xiàn)在是一個(gè)從（J-F）KP到J的函數(shù)?，F(xiàn) 在的轉(zhuǎn)換規(guī)則形式如下： 當(dāng)前狀態(tài)菜單+事件所選擇的項(xiàng)+謂詞 下個(gè)狀態(tài) 第四章形式化說明技術(shù) 4.2.2例子例子 自然語言描述的對(duì)電梯系統(tǒng)的需求。 在一幢m層的大廈中需要一套控制n部電梯的 產(chǎn)品，要求這n部電梯按照約束條件C1 ，C2 和C3在樓層間移動(dòng)。 C1 ：每部電梯內(nèi)有m個(gè)按鈕，每個(gè)按鈕代表 一個(gè)樓層。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈 亮，同時(shí)電梯駛向相應(yīng)的樓層，到達(dá)按鈕指 定的樓層時(shí)指示燈熄滅。 第四章形式化說明技術(shù) 4.2.2例子例子 C2 ：除了大廈的最低層和最高層之外，每層 樓都有兩個(gè)按鈕

8、分別請(qǐng)求電梯上行和下行。 這兩個(gè)按鈕之一被按下時(shí)相應(yīng)的指示燈亮， 當(dāng)電梯到達(dá)此樓層時(shí)燈熄滅，電梯向要求的 方向移動(dòng)。 C3 ：當(dāng)對(duì)電梯沒有請(qǐng)求時(shí)，它關(guān)門并停在當(dāng) 前樓層。 第四章形式化說明技術(shù) 4.2.2例子例子 分析： n部電梯中的每一部都有m個(gè)按鈕，一個(gè)按鈕 對(duì)應(yīng)一個(gè)樓層。因?yàn)檫@m*n個(gè)按鈕都在電梯中， 所以稱它們?yōu)殡娞莅粹o。 每層樓有兩個(gè)按鈕，一個(gè)請(qǐng)求向上，另一個(gè) 請(qǐng)求向下，所以稱它們?yōu)闃菍影粹o。 第四章形式化說明技術(shù) 電梯按鈕的狀態(tài)轉(zhuǎn)換圖電梯按鈕的狀態(tài)轉(zhuǎn)換圖 圖4.1 電梯按鈕的狀態(tài)轉(zhuǎn)換圖 EB（e,f）：表示按下電梯e內(nèi)的按鈕，并請(qǐng)求到f 層去。有兩個(gè)狀態(tài)： -EBON（e,f）：電

9、梯按鈕（e,f）打開 -EBOFF（e,f）：電梯按鈕（e,f）關(guān)閉 兩個(gè)事件： -EBP（e,f）：電梯按鈕（e,f）被按下 - EAF（e,f）：電梯e到達(dá)f層 第四章形式化說明技術(shù) 形式化轉(zhuǎn)換規(guī)則形式化轉(zhuǎn)換規(guī)則 V（e,f）：電梯e停在f層 EBOFF（e,f）+EBP（e,f）+not V（e,f） EBON（e,f） EBON（e,f）+EAF（e,f） EBOFF（e,f） 第四章形式化說明技術(shù) 樓層按鈕的狀態(tài)轉(zhuǎn)換圖樓層按鈕的狀態(tài)轉(zhuǎn)換圖 圖4.3樓層按鈕的狀態(tài)轉(zhuǎn)換圖 FB（d,f）：表示f層請(qǐng)求電梯向d方向運(yùn)動(dòng)的按鈕。 有兩個(gè)狀態(tài)： -FBON（d,f）：樓層按鈕（d,f）打開 -

10、FBOFF（d,f）：樓層按鈕（d,f）關(guān)閉 兩個(gè)事件： - FBP（d,f）：樓層按鈕（d,f）被按下 - EAF（1n,f）：電梯1或或n到達(dá)f層 第四章形式化說明技術(shù) 形式化轉(zhuǎn)換規(guī)則形式化轉(zhuǎn)換規(guī)則 S（d，e，f）：電梯e停在f層并且移動(dòng) 方向由d確定為向上（d=U）或向下（ d=D）或待定（d=N）。 FBOFF（d,f）+ FBP（d,f）+not S（d ，1n，f） FBON（d,f） FBON（d,f）+ EAF（1n,f）+ S（d ，1n，f） FBOFF（d,f） 其中d=UorD 第四章形式化說明技術(shù) 電梯的狀態(tài)轉(zhuǎn)換電梯的狀態(tài)轉(zhuǎn)換 電梯的3個(gè)狀態(tài)： M（d，e，f）：電

11、梯e沿著d方向移動(dòng)，即將到達(dá) 的是第f層 S（d，e，f）：電梯e停在f層，將朝d方向移動(dòng) （尚未關(guān)門） W（e，f）：電梯e在f層等待（已關(guān)門） 電梯的3個(gè)事件： DC（e，f）：電梯e在樓層f關(guān)上門 ST （e，f）：電梯e靠近f層時(shí)觸發(fā)傳感器，電梯 控制器決定在當(dāng)前樓層電梯是否停下 RL：電梯按鈕或樓層按鈕被按下進(jìn)入打開狀態(tài) 第四章形式化說明技術(shù) 電梯的狀態(tài)轉(zhuǎn)換圖電梯的狀態(tài)轉(zhuǎn)換圖 圖4.4電梯的狀態(tài)轉(zhuǎn)換圖 第四章形式化說明技術(shù) 形式化轉(zhuǎn)換規(guī)則形式化轉(zhuǎn)換規(guī)則 S（U，e，f）+DC（e，f） M（U，e，f+1） S（D，e，f）+DC（e，f） M（D，e，f-1） S（N，e，f）+D

12、C（e，f） W（e，f） 第四章形式化說明技術(shù) 4 . 2 . 3 評(píng)價(jià)評(píng)價(jià) 分析它的簡(jiǎn)單格式描述規(guī)格說明： 當(dāng)前狀態(tài)+事件+謂詞=下個(gè)狀態(tài) 第四章形式化說明技術(shù) 4.3 Petri網(wǎng)網(wǎng) 4.3.1概念 并發(fā)系統(tǒng)中遇到的一個(gè)主要問題? 它的表現(xiàn)形式? 已經(jīng)證明：Petri 網(wǎng)可以有效地描述并發(fā)活動(dòng)。 第四章形式化說明技術(shù) 4.3.1概念概念 4.3.1概念（描述并發(fā)活動(dòng)、處理定時(shí)需求） 四元組C=（P,T,I,O） P=P1,Pn是一個(gè)有窮位置集，n0 T =t1,tm 是一個(gè)有窮轉(zhuǎn)換集，m0 I：TP為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位 組的映射 O：TP 為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單

13、位組的映射 一個(gè)無序單位組或多重組是允許一個(gè)元素有多個(gè) 實(shí)例的廣義集 第四章形式化說明技術(shù) 4.3.1概念概念 圖4.5 Petri網(wǎng)的組成 第四章形式化說明技術(shù) 4.3.1概念概念 圖4.6帶標(biāo)記的Petri網(wǎng) 第四章形式化說明技術(shù) 4.3.1概念概念 圖4.7圖4.6的Petri網(wǎng)在轉(zhuǎn)換t1被激發(fā)后的情況 第四章形式化說明技術(shù) 4.3.1概念概念 圖4.8圖4.7的Petri網(wǎng)在轉(zhuǎn)換t2被激發(fā)后的情況 第四章形式化說明技術(shù) 4.3.1概念概念 圖4.9含禁止線的Petri網(wǎng) 第四章形式化說明技術(shù) 4 . 3 . 2 例子例子 圖4.10 Petri網(wǎng)表示的電梯按鈕圖4.10 Petri網(wǎng)表

14、示的電梯按鈕圖4.10 Petri網(wǎng)表示的電梯按鈕圖4.10 Petri網(wǎng)表示的電梯按鈕圖4.10 Petri網(wǎng)表示的電梯按鈕1. 電梯按鈕 圖4.10 Petri網(wǎng)表示的電梯按鈕 1：電梯按鈕 第四章形式化說明技術(shù) 4 . 3 . 2 例子例子 2：樓層按鈕 圖4.11Petri網(wǎng)表示樓層按鈕 圖4.11 Petri網(wǎng)表示的樓層按鈕 第四章形式化說明技術(shù) 4.4 Z語言語言 4.4.1簡(jiǎn)介 1. 給定的集合 2. 狀態(tài)定義 4.4.1簡(jiǎn)介4.4.1簡(jiǎn)介 1. 給定的集合 2. 狀態(tài)定義 第四章形式化說明技術(shù) 2. 狀態(tài)定義狀態(tài)定義 圖4.12 Z格S的格式 第四章形式化說明技術(shù) 2. 狀態(tài)定

15、義狀態(tài)定義 圖4.13Z格Button_State圖4.12Z格S的格式 圖4.13Z格Button_State 第四章形式化說明技術(shù) 4.4.1簡(jiǎn)介圖簡(jiǎn)介圖 3. 初始狀態(tài) 4. 操作 圖4.14操作Push_Button的Z規(guī)格說明圖4.14操作Push_Button的Z規(guī)格說明 4.14 操作Push_Button的Z規(guī)格說明 第四章形式化說明技術(shù) 4. 操作操作 4.15 操作Floor_Arrival的Z規(guī)格說明Floor_Arrival的Z規(guī)格說明 第四章形式化說明技術(shù) 4.4.2評(píng)價(jià)評(píng)價(jià) Z語言之所以會(huì)獲得如此多的成功， 主要有 以下原因： 1：較容易發(fā)現(xiàn)用Z寫的規(guī)格說明的錯(cuò)誤。 2：精確性要求較高，減少了模糊性、不一致 性和遺漏。 3：在需要時(shí)開發(fā)者可以嚴(yán)格地驗(yàn)證規(guī)格說明 的正確性。 4：可以較短時(shí)間就學(xué)會(huì)Z規(guī)格說明。 第四章形