1、軟件工程2022/7/272第四章 形式化說明技術Why Formal? 自然語言：矛盾、二義性、含糊 形式化表示：準確、清晰 非形式化：自然語言 半形式化：DFD、E-R圖 形式化：堅實的以數(shù)學為基礎的表示方法2022/7/273第四章 形式化說明技術4.1 概述4.2 有窮狀態(tài)機4.3 Petri網4.4 Z語言2022/7/2744.1 概述4.1.1 非形式化方法的缺點矛盾：相互沖突的陳述二義性：讀者可以用不同的方式理解的陳述含糊不完整抽象層次混亂：非常抽象的陳述中混進了一些關于細節(jié)的低層次陳述。2022/7/2754.1 概 述4.1.2 形式化方法的優(yōu)點把數(shù)學引入軟件開發(fā)過程，形成

2、基于數(shù)學的形式化方法。數(shù)學最有用的一個性質是，能夠簡潔準確地描述物理現(xiàn)象、對象或動作的結果，因此是理想的建模工具。在軟件開發(fā)過程中使用數(shù)學，可以在不通的軟件工程活動之間平滑地過渡。提供了高層確認的手段。2022/7/2764.1 概 述4.1.3 應用形式化方法的準則應該選用適當?shù)谋硎痉椒☉撔问交灰^分形式化應該估算成本應該有形式化方法顧問隨時提供咨詢不應該放棄傳統(tǒng)的開發(fā)方法應該建立詳盡的文檔不應該放棄質量標準不應該盲目依賴形式化方法應該測試、測試再測試應該重用2022/7/2774.2 有窮狀態(tài)機4.2.1 概念一個保險箱上裝了一個復合鎖，鎖有3個位置，分別標記為1、2、3，轉盤可向

3、左（L）或向右（R）轉動。這樣，任何時刻轉盤都有6種可能的運動，即1L、1R、2L、2R、3L、3R。保險箱的組合密碼是1L、3R、2L，轉盤的任何其他運動都將引起報警。2022/7/2784.2 有窮狀態(tài)機圖4.1 保險箱的狀態(tài)轉換圖2022/7/2794.2 有窮狀態(tài)機2022/7/27104.2 有窮狀態(tài)機一個有窮狀態(tài)機包括5個部分：狀態(tài)集J：保險箱鎖定，A，B，保險箱解鎖， 報警輸入集K：1L、1R、2L、2R、3L、3R轉換函數(shù)T：如表4.1所示初始態(tài)S：保險箱鎖定終態(tài)集F：保險箱解鎖，報警2022/7/27114.2 有窮狀態(tài)機一個有窮狀態(tài)機可以表示為一個5元組（J，K，T，S，F(xiàn)

4、），其中：J是一個有窮的非空狀態(tài)集；K是一個有窮的非空輸入集；T是一個從（J-F）*K到J的轉換函數(shù)；SJ，是一個初始狀態(tài)；F J，是終態(tài)集一個有窮狀態(tài)機可以表示為一個5元組（J，K，T，S，F(xiàn)），其中：J是一個有窮的非空狀態(tài)集；K是一個有窮的非空輸入集；T是一個從（J-F）*K到J的轉換函數(shù)；SJ，是一個初始狀態(tài)；F J，是終態(tài)集2022/7/27124.2 有窮狀態(tài)機加入謂詞集P，把有窮狀態(tài)機擴展為一個6元組，其中每個謂詞都是系統(tǒng)全局狀態(tài)Y的函數(shù)。則轉換函數(shù)T：（J-F）*K*P J2022/7/27134.2 有窮狀態(tài)機4.2.2 例子電梯按鈕EB（e，f）：按下電梯e內的按鈕并請求到f

5、層去狀態(tài)：EBON（e，f）：電梯按鈕（e，f）打開EBOFF（e，f）：電梯按鈕（e，f）關閉事件EBP （e，f）：電梯按鈕（e，f）被按下EAF （e，f）：電梯到達f層謂詞V （e，f）：電梯e停在f層2022/7/27144.2 有窮狀態(tài)機圖4.2 電梯按鈕的狀態(tài)轉換圖 2022/7/27154.2 有窮狀態(tài)機樓層按鈕FB（d，f）：f層請求電梯向d方向運動的按鈕狀態(tài)：FBON（d，f）：樓層按鈕（d，f）打開FBOFF（d，f） ：樓層按鈕（d，f）關閉事件FBP （d，f）：樓層按鈕（d，f）被按下EAF（1n，f）：電梯1或或n到達f層謂詞S（d，e，f）：電梯e停在f層并且移

6、動方向由d確定2022/7/27164.2 有窮狀態(tài)機圖4.3 樓層按鈕的狀態(tài)轉換圖 2022/7/27174.2 有窮狀態(tài)機電梯狀態(tài)M（d，e，f）：電梯e正沿d方向移動，即將到達的是第f層S（ d，e，f ）：電梯e停在f層，將朝d方向移動（尚未關門）W（e，f）：電梯e在f層等待（已關門）事件DC（ e，f ）：電梯e在樓層f關上門ST（ e，f ）：電梯e靠近f層時觸發(fā)傳感器，電梯控制器決定在當前樓層電梯是否停下RL：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)，登錄需求2022/7/27184.2 有窮狀態(tài)機圖4.4 電梯的狀態(tài)轉換圖 2022/7/27194.2 有窮狀態(tài)機關門之時的規(guī)則2

7、022/7/2720思考題定義狀態(tài)：O（e，f）：電梯e在f層開門，則如何進入這個狀態(tài)從等待到移動，如何表示2022/7/27214.2 有窮狀態(tài)機4.2.3 評價有窮狀態(tài)機描述規(guī)格說明：當前狀態(tài)+事件+謂詞 下個狀態(tài)優(yōu)點：易于書寫、易于驗證、精確、易于理解缺點：開發(fā)大系統(tǒng)時三元組的數(shù)量會迅速增長沒有處理定時的需求2022/7/27224.3 Petri網4.3.1 概述并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題同步問題競爭條件死鎖Petri網是一種用于確定系統(tǒng)中隱含的定時問題的一種有效技術可有效的描述并發(fā)活動2022/7/27234.3 Petri網包含元素位置P：P1 ，P2 ，P3 ，P4轉

8、換T：t1，t2圖4.5 Petri網的組成 輸入函數(shù)I：I（ t1 ）= P2 ，P4I（ t2 ）= P2輸出函數(shù)OO（ t1 ）= P1O（ t2 ）= P3 ，P32022/7/27244.3 Petri網更形式化的Petri網結構，是一個四元組C=（P，T，I，O）其中，P=P1，Pn是一個有窮位置集，n=0T=t1，tm是一個有窮轉換集，m=0，且T和P不相交。I： 為輸入函數(shù)，是由轉換到位置無序單位組的映射。O： 為輸出函數(shù)，是由轉換到位置無序單位組的映射。2022/7/27254.3 Petri網Petri網的標記是在Petri網中權標(token)的分配。圖4.6 帶標記的P

9、etri網（1，2，0，1）圖4.7 圖4.6的Petri網在轉換t1被激發(fā)后的情況（2，1，0，0） 圖4.8 圖4.7的Petri網在轉換t2被激發(fā)后的情況（2，0，2，0）2022/7/27264.3 Petri網對Petri網的一個重要擴充是加入禁止線。禁止線是用一個小圓圈而不是用箭頭標記的輸入線。通常，當每個輸入線上至少有一個令牌，而禁止線上沒有令牌的時候，相應的轉換才是允許的。圖4.9 含禁止線的Petri網2022/7/27274.3 Petri網4.3.2 例子每個樓層用一個位置Ff代表(1fm)電梯是用一個權標代表。在位置Ff上有權標，表示在樓層f上有電梯。2022/7/27

10、284.3 Petri網1.電梯按鈕電梯中樓層f的按鈕，在Petri網中用位置EBf表示(1fm)。在EBf上有一個令牌，就表示電梯內樓層f的按鈕被按下了。2022/7/27294.3 Petri網2.樓層按鈕在Petri網中樓層按鈕用位置 和 表示，分別代表f樓層請求電梯上行和下行的按鈕。2022/7/27304.4 Z語言4.4.1 簡介用Z語言描述的、最簡單的形式化規(guī)格說明含有下述4個部分。給定的集合、數(shù)據(jù)類型及常數(shù)。狀態(tài)定義。初始狀態(tài)。操作。2022/7/27314.4 Z語言1.給定的集合從一系列給定的初始化集合開始。即不需要詳細定義的集合，這種集合用帶方括號的形式表示。Button

11、2022/7/27324.4 Z語言2.狀態(tài)定義一個Z規(guī)格說明由若干個“格(schema)”組成，每個格含有一組變量說明和一系列限定變量取值范圍的謂詞。2022/7/27334.4 Z語言圖4.13描述了格Button_State符號P表示冪集(即給定集的所有子集)。約束條件聲明，floor_buttons集與elevator_buttons集不相交，而且它們共同組成buttons集圖4.13 Z格Button_State 2022/7/27344.4 Z語言3.初始狀態(tài)抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。Button_Init Button_Statepushed= 4.操作如果一個原

12、來處于關閉狀態(tài)的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到pushed集中。2022/7/27354.4 Z語言假設電梯到達了某樓層，如果相應的樓層按鈕已經打開，則此時它會關閉；同樣，如果相應的電梯按鈕已經打開，則此時它也會關閉。2022/7/27364.4 Z語言4.4.2 評價Z作為應用得最廣泛的形式化語言，在大型項目中的優(yōu)勢更加明顯。Z語言之所以會獲得如此多的成功，主要有以下幾個原因：（1）可以比較容易地發(fā)現(xiàn)用Z寫的規(guī)格說明的錯誤；（2）用Z寫規(guī)格說明時，要求作者十分精確地使用Z說明符。2022/7/27374.4 Z語言（3）Z是一種形式化語言，在需要時開發(fā)者可以嚴格地驗證規(guī)格說明的正確性。（4）雖然完全學會Z語言相當困難，但是，經驗表明，只學過中學數(shù)學的軟件開發(fā)人員仍然可以只用比較短的時間就學會編寫Z規(guī)格說明，當然，這些人還沒有能力證明規(guī)格說明的結果是否正確。（5）使用Z語言可以降低軟件開發(fā)費用