形式化說明技術

1、第第4章章 形式化說明技術形式化說明技術(Formalization Method)非形式化：用自然語言描述的需求說明非形式化：用自然語言描述的需求說明半形式化：用半形式化：用DFD、ER圖建立的模型圖建立的模型形式化方法形式化方法：是描述系統(tǒng)性質的、基于數(shù)學的技術：是描述系統(tǒng)性質的、基于數(shù)學的技術 本章在介紹非形式化方法不足的基礎上，介紹了形本章在介紹非形式化方法不足的基礎上，介紹了形式化方法的優(yōu)點，及常見的形式化方法：有窮狀態(tài)機、式化方法的優(yōu)點，及常見的形式化方法：有窮狀態(tài)機、Petri網、網、Z語言。語言。 形式化方法基本含義是借助數(shù)學的方法來研究計算機科學形式化方法基本含義是借助數(shù)學的

2、方法來研究計算機科學中的有關問題。中的有關問題。 Encyclopedia of Software Engineering對形式化方法定對形式化方法定義：用于開發(fā)計算機系統(tǒng)的形式化方法是基于數(shù)學的用于描義：用于開發(fā)計算機系統(tǒng)的形式化方法是基于數(shù)學的用于描述系統(tǒng)性質的技術。它提供了一個框架，可以在該框架中以述系統(tǒng)性質的技術。它提供了一個框架，可以在該框架中以系統(tǒng)的方式刻畫、開發(fā)和驗證系統(tǒng)。系統(tǒng)的方式刻畫、開發(fā)和驗證系統(tǒng)。 因此因此：在軟件開發(fā)全過程中，凡是采用嚴格的數(shù)學語言，：在軟件開發(fā)全過程中，凡是采用嚴格的數(shù)學語言，具有精確的數(shù)學語義的方法，都稱為形式化方法。包括具有精確的數(shù)學語義的方法，都

3、稱為形式化方法。包括形式形式化規(guī)格化規(guī)格（Specification）和）和形式化驗證形式化驗證（Verification）。）。形式化說明技術形式化說明技術1. 概概 述述1、非形式化方法的缺點、非形式化方法的缺點 陳述的前后矛盾陳述的前后矛盾 理解的二義性理解的二義性 不精確性不精確性 不完整性不完整性 抽象層次混亂抽象層次混亂2、形式化方法的優(yōu)點、形式化方法的優(yōu)點 能簡潔準確描述物理現(xiàn)象、對象或動作的結果能簡潔準確描述物理現(xiàn)象、對象或動作的結果 可在不同軟件工程活動之間平滑過渡可在不同軟件工程活動之間平滑過渡 提供了高層確認的手段提供了高層確認的手段1. 概述概述3、應用形式化方法的準則

4、、應用形式化方法的準則 應該選用適當?shù)男问交f明方法應該選用適當?shù)男问交f明方法 應該形式化，但不要過分形式化應該形式化，但不要過分形式化 應該預先估算使用形式化方法的成本應該預先估算使用形式化方法的成本 應該有形式化方法的顧問隨時提供咨詢應該有形式化方法的顧問隨時提供咨詢 盡量與傳統(tǒng)方法結合起來使用盡量與傳統(tǒng)方法結合起來使用 應該建立詳盡的文檔應該建立詳盡的文檔 應該一如既往地實施其他質量保證活動應該一如既往地實施其他質量保證活動 不要盲目依賴形式化方法不要盲目依賴形式化方法 應該測試、測試、再測試應該測試、測試、再測試 應該堅持軟件重用應該堅持軟件重用結束2. 有窮狀態(tài)機有窮狀態(tài)機客觀世界

5、中，存在大量具有有限個狀態(tài)的系統(tǒng)，如客觀世界中，存在大量具有有限個狀態(tài)的系統(tǒng)，如 商場自動門控制器商場自動門控制器 保險箱開鎖保險箱開鎖 鐘表狀態(tài)鐘表狀態(tài) 飲料自動售貨機飲料自動售貨機1、基本概念、基本概念 一個有窮狀態(tài)機可以表示為一個五元組（一個有窮狀態(tài)機可以表示為一個五元組（J，K，T，S，F(xiàn)），），其中：其中： J：有窮的非空狀態(tài)集：有窮的非空狀態(tài)集 K：有窮的非空輸入集：有窮的非空輸入集 S：初始狀態(tài)，：初始狀態(tài)，S J F：終態(tài)集，：終態(tài)集， F J T：狀態(tài)轉換函數(shù)：狀態(tài)轉換函數(shù) (J - F) K J 實際對系統(tǒng)進行規(guī)格說明時常進行擴展，即增加一個謂詞集實際對系統(tǒng)進行規(guī)格說明時常

6、進行擴展，即增加一個謂詞集P，狀態(tài)轉換函數(shù)擴展為：狀態(tài)轉換函數(shù)擴展為：(J - F) K P J 當前狀態(tài)當前狀態(tài) + 事件事件 + 謂詞謂詞 下一狀態(tài)下一狀態(tài) 當前狀態(tài)當前狀態(tài) + 事件事件 下一狀態(tài)下一狀態(tài)2. 有窮狀態(tài)機有窮狀態(tài)機例如一個開保險箱的有窮狀態(tài)機表示為例如一個開保險箱的有窮狀態(tài)機表示為(J，K，T，S，F(xiàn))，其中：其中： J：保險箱鎖定，保險箱鎖定，A，B，保險箱解鎖，報警，保險箱解鎖，報警 K：1L，1R，2L，2R，3L，3R S：保險箱鎖定：保險箱鎖定 F：保險箱解鎖，報警保險箱解鎖，報警 T：狀態(tài)轉換函數(shù)如下：狀態(tài)轉換函數(shù)如下保險箱鎖定保險箱鎖定AB1LA報警報警報警

7、報警1R報警報警報警報警報警報警2L報警報警報警報警保險箱解鎖保險箱解鎖2R報警報警報警報警報警報警3L報警報警報警報警報警報警3R報警報警B報警報警2. 有窮狀態(tài)機有窮狀態(tài)機保險箱保險箱鎖鎖 定定BA保險箱保險箱解解 鎖鎖報報 警警初初始始態(tài)態(tài)1L終終態(tài)態(tài)3R終態(tài)終態(tài)2L 其他其他移動移動 其他其他移動移動 其他其他移動移動有窮狀態(tài)機的狀態(tài)轉換圖有窮狀態(tài)機的狀態(tài)轉換圖2. 有窮狀態(tài)機有窮狀態(tài)機2. 有窮狀態(tài)機有窮狀態(tài)機2、應用例子、應用例子電梯問題電梯問題P.79EBON(e,f)：電梯按鈕：電梯按鈕(e,f)打開打開EBOFF(e,f)：電梯按鈕：電梯按鈕(e,f)關閉關閉EBP(e,f)

8、：電梯按鈕：電梯按鈕(e,f)被按下被按下EAF(e,f)：電梯：電梯e到達到達f層層EBOFF(e,f)EBON(e,f)EBP(e,f)EAF(e,f)(1) 電梯按鈕的狀態(tài)轉換圖：電梯按鈕的狀態(tài)轉換圖：謂詞謂詞V(e,f)：電梯：電梯e停在停在f層層狀態(tài)轉換狀態(tài)轉換規(guī)則規(guī)則：EBOFF(e,f) + EBP(e,f) + not V(e,f) EBON(e,f)EBON(e,f) + EAF(e,f) EBOFF(e,f)2. 有窮狀態(tài)機有窮狀態(tài)機FBON(d,f)：樓層按鈕：樓層按鈕(d,f)打開打開FBOFF(d,f)：樓層按鈕：樓層按鈕(d,f)關閉關閉FBP(d,f)：樓層按鈕：

9、樓層按鈕(d,f)被按下被按下FAF(1.n,f)：電梯：電梯1或或或或n到達到達f層層FBOFF(d,f)FBON(d,f)FBP(d,f)EAF(1.n,f)(2) 樓層按鈕的狀態(tài)轉換圖：樓層按鈕的狀態(tài)轉換圖：謂詞謂詞S(d,e,f)：電梯：電梯e停在停在f層并且移動方向由層并且移動方向由d確定確定(U,D,N)狀態(tài)轉換狀態(tài)轉換規(guī)則規(guī)則(d = U or D)：FBOFF(d,f) + FBP(d,f) + not S(d,1.n,f) FBON(d,f)FBON(d,f) + EAF(1.n,f) + S(d,1.n,f) EBOFF(e,f)2. 有窮狀態(tài)機有窮狀態(tài)機狀態(tài)狀態(tài)：M(d,

10、e,f)：電梯：電梯e正沿正沿d方向移動，即方向移動，即將到達將到達f層層S(d,e,f)：電梯：電梯e停在停在f層，將向層，將向d方向方向移動移動(未關門未關門)W(e,f)：電梯：電梯e在在f層等待層等待(已關門已關門)(3) 電梯的狀態(tài)轉換圖：電梯的狀態(tài)轉換圖：狀態(tài)轉換狀態(tài)轉換規(guī)則規(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) + DC(e,f) W(e,f) 事件事件：DC(e,f)：電梯：電梯e正樓層正樓層f關上門關上門ST(e,f)：電梯：電梯e靠近靠近f層時觸發(fā)傳感器，層時觸發(fā)傳感器，電梯

11、控制器決定是否停下電梯控制器決定是否停下RL：電梯按鈕或樓層按鈕被按下進：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)，登錄需求入打開狀態(tài)，登錄需求M(U,e,f+1)DC(e,f)M(U,e,f)M(D,e,f)M(D,e,f-1)W(e,f)S(U,e,f)S(N,e,f)S(D,e,f)RLRLDC(e,f)RLRLRLDC(e,f)ST(e,f)ST(e,f)3、有窮狀態(tài)機的評價、有窮狀態(tài)機的評價2. 有窮狀態(tài)機有窮狀態(tài)機 描述形式化規(guī)格說明方法簡單描述形式化規(guī)格說明方法簡單 當前狀態(tài)當前狀態(tài) + 事件事件 + 謂詞謂詞 下一個狀態(tài)下一個狀態(tài) 規(guī)格說明易于書寫、驗證規(guī)格說明易于書寫、驗證 可以

12、較容易將規(guī)格說明轉變成設計或程序可以較容易將規(guī)格說明轉變成設計或程序 對軟件便于維護對軟件便于維護 有窮狀態(tài)機比有窮狀態(tài)機比DFD描述更精確描述更精確 有窮狀態(tài)機處理大系統(tǒng)開發(fā)時會變得困難有窮狀態(tài)機處理大系統(tǒng)開發(fā)時會變得困難 有窮狀態(tài)機無法處理定時需求有窮狀態(tài)機無法處理定時需求3. Petri 網網 Petri網是由德國的網是由德國的Carl Adam Petri于于1962年在其博士論年在其博士論文文“自動機通信自動機通信”中提出的，它是一種適合于中提出的，它是一種適合于并發(fā)并發(fā)、異步異步、分布式分布式軟件系統(tǒng)規(guī)格與分析的形式化方法。軟件系統(tǒng)規(guī)格與分析的形式化方法。 任何系統(tǒng)都可抽象為狀態(tài)、

13、活動（或事件）及其之間關任何系統(tǒng)都可抽象為狀態(tài)、活動（或事件）及其之間關系的三元結構。在系的三元結構。在Petri網中，狀態(tài)用網中，狀態(tài)用位置位置表示，活動用表示，活動用轉換轉換表示。轉換的作用是改變狀態(tài)，位置的作用是決定轉換能否表示。轉換的作用是改變狀態(tài)，位置的作用是決定轉換能否發(fā)生，轉換和位置之間的這種依賴關系用輸入輸出函數(shù)（流發(fā)生，轉換和位置之間的這種依賴關系用輸入輸出函數(shù)（流關系）來表示。關系）來表示。1、基本概念、基本概念 一個一個Petri網結構，是一個四元組網結構，是一個四元組(P，T，I，O)，其中：，其中： P：有窮的非空位置集（庫所）：有窮的非空位置集（庫所） T：有窮的非

14、空轉換集（遷移），且：有窮的非空轉換集（遷移），且P T= I：輸入函數(shù)：輸入函數(shù) T P O：輸出函數(shù)：輸出函數(shù) T P p1p2p4p3t2t1 P：p1,p2,p3,p4 T：t1,t2 I：I(t1)=p2,p4 I(t2)=p2 O：O(t1)=p1 O(t2)=p3,p33. Petri網網3. Petri網網Petri網描述系統(tǒng)動態(tài)行為機制：網描述系統(tǒng)動態(tài)行為機制： 帶標記的帶標記的Petri網是一個五元組網是一個五元組(P，T，I，O，M)，其中：，其中： P、T、I、O同前；同前； M稱稱Petri網的標記（令牌），它是網的標記（令牌），它是Petri網中權標的分配。網中權標

15、的分配。 M：P 0，1，2，p1p2p4p3t2t1注意注意： 激發(fā)轉換的條件：每個激發(fā)轉換的條件：每個輸入位置擁有的權標數(shù)輸入位置擁有的權標數(shù)大于等于從該位置到轉大于等于從該位置到轉換的線數(shù)。換的線數(shù)。 Petri網具有不確定性網具有不確定性 Petri網中權標總數(shù)不是網中權標總數(shù)不是固定的固定的3. Petri網網p1p2p4p3t2t1p1p2p4p3t2t1p1p2p4p3t2t1Petri網的擴充：網的擴充：加入禁止線加入禁止線 ，表示沒有權標才激發(fā)轉換。表示沒有權標才激發(fā)轉換。Petri網具有描述順序、并發(fā)、網具有描述順序、并發(fā)、沖突、混惑等結構行為能力。沖突、混惑等結構行為能力

16、。3. Petri網網2、例子、例子電梯問題電梯問題(1) 電梯按鈕電梯按鈕EBfFg電梯在運行電梯在運行FfEBf被按下被按下FBfUFg電梯在運行電梯在運行FfFBfU被按下被按下FBfD電梯在運行電梯在運行FfFBfD被按下被按下(2) 樓層按鈕樓層按鈕EBf：電梯中樓層：電梯中樓層f的按鈕的按鈕Ff：樓層：樓層fFg：樓層：樓層gFBfU：樓層：樓層f上行按鈕上行按鈕FBfD：樓層：樓層f下行按鈕下行按鈕Ff：樓層：樓層fFg：樓層：樓層g注意注意： 標準標準Petri網的轉換是瞬時網的轉換是瞬時完成的完成的 這里考慮的是簡化情況這里考慮的是簡化情況4. Z 語言語言1、Z 語言簡介語

17、言簡介用用Z語言描述的，最簡單的形式化規(guī)格說明包含語言描述的，最簡單的形式化規(guī)格說明包含4個部分：個部分： 給定的集合、數(shù)據類型及常數(shù)給定的集合、數(shù)據類型及常數(shù) 狀態(tài)定義狀態(tài)定義 初始狀態(tài)初始狀態(tài) 操作操作 （1）給定的集合）給定的集合 Z規(guī)格說明從一系列給定的初始化集合開始。規(guī)格說明從一系列給定的初始化集合開始。 初始化集合初始化集合是不需要詳細定義的集合，用方括號形式表示。是不需要詳細定義的集合，用方括號形式表示。 如電梯問題中，給定的初始化集合為如電梯問題中，給定的初始化集合為Button，表示為，表示為 Button4. Z 語言語言 （2）狀態(tài)定義）狀態(tài)定義 一個一個Z規(guī)格說明由若干

18、個規(guī)格說明由若干個“格格”組成，每個格含有一組變量組成，每個格含有一組變量說明和一系列限定變量取值范圍的謂詞。表示為說明和一系列限定變量取值范圍的謂詞。表示為S說明說明謂詞謂詞Button_Statefloor_buttons，elevator_buttons : P Buttonbuttons : P Buttonpushed : P Buttonfloor_buttons elevator_buttons = floor_buttons elevator_buttons = buttons例如電梯問題中的例如電梯問題中的Z格格Button_State：4. Z 語言語言 （3）初始狀態(tài)）初始狀態(tài) 初始狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。如初始狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。如Button_Init Button_State | pushed = =Push_Button Button_Statebutton ? : Button(button ? buttons) (button ? pushed) (pushed = pushed button ? ) (button ? pushed) (pus