1、第第4章章 形式化說明技術形式化說明技術4.1 概述概述4.2 有窮狀態機有窮狀態機4.3 Petri網網4.4 Z語言語言4.5 小結小結1.形式化方法定義形式化方法定義 描述系統性質的基于數學的技術，也就是說，如果一種方法有堅實的數學基礎，那描述系統性質的基于數學的技術，也就是說，如果一種方法有堅實的數學基礎，那么它就是形式化的。么它就是形式化的。2.分類分類 按照形式化的程度分成非形式化、半形式化和形式化按照形式化的程度分成非形式化、半形式化和形式化3類。類。 非形式化方法：用自然語言描述需求規格說明。非形式化方法：用自然語言描述需求規格說明。 半形式化方法：用數據流圖或實體半形式化方法

2、：用數據流圖或實體-聯系圖建立模型。聯系圖建立模型。 用自然語言書寫的系統規格說明書，可能存在矛盾、二義性、含糊性、不完整性及用自然語言書寫的系統規格說明書，可能存在矛盾、二義性、含糊性、不完整性及抽象層次混亂等問題。抽象層次混亂等問題。 矛盾：是指一組相互沖突的陳述。矛盾：是指一組相互沖突的陳述。 二義性：是指讀者可以用不同方式理解的陳述。二義性：是指讀者可以用不同方式理解的陳述。4.1 概述概述 4.1.1 非形式化方法的缺點非形式化方法的缺點含糊性：系統規格說明書是很龐大的文檔，因此，幾乎不可避免地會出現含糊性。含糊性：系統規格說明書是很龐大的文檔，因此，幾乎不可避免地會出現含糊性。不完

3、整性：可能是在系統規格說明中最常遇到的問題之一。不完整性：可能是在系統規格說明中最常遇到的問題之一。抽象層次混亂：是指在非常抽象的陳述中混進了一些關于細節的低層次陳述。這樣的規抽象層次混亂：是指在非常抽象的陳述中混進了一些關于細節的低層次陳述。這樣的規格說明書使得讀者很難了解系統的整體功能結構。格說明書使得讀者很難了解系統的整體功能結構。 形式化方法：為了克服非形式化方法的缺點，人們把數學引入軟件開發過程，創造了形式化方法：為了克服非形式化方法的缺點，人們把數學引入軟件開發過程，創造了基于數學的形式化方法。基于數學的形式化方法。 在開發大型軟件系統的過程中應用數學，能夠帶來下述的幾個優點：在開

4、發大型軟件系統的過程中應用數學，能夠帶來下述的幾個優點： 1.數學能夠簡潔準確地描述物理現象、對象或動作的結果，因此是理想的建模工具。數學能夠簡潔準確地描述物理現象、對象或動作的結果，因此是理想的建模工具。 2.數學特別適合于表示狀態，也就是表示數學特別適合于表示狀態，也就是表示“做什么做什么”。4.1.2 形式化方法的優點形式化方法的優點軟件需求的問題描述：軟件需求的問題描述： 需求規格說明書主要描述應用系統在運行前和運行后的狀態，因此，數學比自然語言需求規格說明書主要描述應用系統在運行前和運行后的狀態，因此，數學比自然語言更適于描述詳細的需求。更適于描述詳細的需求。數學規格說明的優點：數學

5、規格說明的優點： 分析員可以寫出系統的數學規格說明，它準確到幾乎沒有二義性，而且可以用數學分析員可以寫出系統的數學規格說明，它準確到幾乎沒有二義性，而且可以用數學方法來驗證，以發現存在的矛盾和不完整性，在這樣的規格說明中完全沒有含糊性。方法來驗證，以發現存在的矛盾和不完整性，在這樣的規格說明中完全沒有含糊性。形式化分析的問題：形式化分析的問題：1.軟件系統的復雜性是出了名的，希望用少數幾個數學公式來描述它，是根本不可軟件系統的復雜性是出了名的，希望用少數幾個數學公式來描述它，是根本不可能的。能的。2. 即使應用了形式化方法，完整性也是難于保證的：即使應用了形式化方法，完整性也是難于保證的：（1

6、）由于溝通不夠，可能遺漏了客戶的一些需求；）由于溝通不夠，可能遺漏了客戶的一些需求；（2）規格說明的撰寫者可能有意省略了系統的某些特征，以便設計者在選擇實現）規格說明的撰寫者可能有意省略了系統的某些特征，以便設計者在選擇實現方法時有一定自由度；方法時有一定自由度；（3）要設想出使用一個大型復雜系統的每一個可能的情景，通常是做不到的）要設想出使用一個大型復雜系統的每一個可能的情景，通常是做不到的（1）形式化方法對某些軟件工程師很有吸引力，其擁護者甚至宣稱這種方法可以引發軟）形式化方法對某些軟件工程師很有吸引力，其擁護者甚至宣稱這種方法可以引發軟件開發方法的革命；件開發方法的革命；（2）另一些人則

7、對把數學引入軟件開發過程持懷疑甚至反對的態度。）另一些人則對把數學引入軟件開發過程持懷疑甚至反對的態度。（3）對形式化方法也應該）對形式化方法也應該“一分為二一分為二”，既不要過分夸大它的優點也不要一概排斥。，既不要過分夸大它的優點也不要一概排斥。形式化方法的應用形式化方法的應用4.1.3 應用形式化方法的準則應用形式化方法的準則下面給出應用形式化方法的幾條準則：下面給出應用形式化方法的幾條準則：應該選用適當的表示方法。應該選用適當的表示方法。 通常，一種規格說明技術只能用自然的方式說明某一類概念，如果用這種技通常，一種規格說明技術只能用自然的方式說明某一類概念，如果用這種技術描述其不適于描述

8、的概念，則不僅工作量大而且描述方式也很復雜。因此，應該術描述其不適于描述的概念，則不僅工作量大而且描述方式也很復雜。因此，應該仔細選擇一種適用于當前項目的形式化說明技術。仔細選擇一種適用于當前項目的形式化說明技術。(2) 應該形式化，但不要過分形式化。應該形式化，但不要過分形式化。 目前的形式化技術還不適于描述系統的每個方面。目前的形式化技術還不適于描述系統的每個方面。 形式化規格說明技術要求非常準確地描述事物，有助于防止含糊和誤解。形式化規格說明技術要求非常準確地描述事物，有助于防止含糊和誤解。 通常用形式化方法仔細說明系統中易出錯的或關鍵的部分，則只用適中的工作量就通常用形式化方法仔細說明

9、系統中易出錯的或關鍵的部分，則只用適中的工作量就能獲得較大回報。能獲得較大回報。(3) 應該估算成本。應該估算成本。 為了使用形式化方法，通常需要事先進行大量的培訓。最好預先估算所需的成本并編為了使用形式化方法，通常需要事先進行大量的培訓。最好預先估算所需的成本并編入預算。入預算。(4) 應該有形式化方法顧問隨時提供咨詢。應該有形式化方法顧問隨時提供咨詢。 絕大多數軟件工程師對形式化方法中使用的數學和邏輯并不很熟悉，而且沒受過使用絕大多數軟件工程師對形式化方法中使用的數學和邏輯并不很熟悉，而且沒受過使用形式化方法的專業訓練，因此，需要專家指導和培訓。形式化方法的專業訓練，因此，需要專家指導和培

10、訓。(5) 不應該放棄傳統的開發方法。不應該放棄傳統的開發方法。 把形式化方法和結構化方法或面向對象方法集成起來是可能的，而且由于取長把形式化方法和結構化方法或面向對象方法集成起來是可能的，而且由于取長補短往往能獲得很好的效果。補短往往能獲得很好的效果。(6) 應該建立詳盡的文檔。應該建立詳盡的文檔。 建議使用自然語言注釋形式化的規格說明書，以幫助用戶和維護人員理解系統。建議使用自然語言注釋形式化的規格說明書，以幫助用戶和維護人員理解系統。(7) 不應該放棄質量標準。不應該放棄質量標準。 形式化方法并不能保證軟件的正確性，它們只不過是有助于開發出高質量軟件的一形式化方法并不能保證軟件的正確性，

11、它們只不過是有助于開發出高質量軟件的一種手段。除了使用形式化說明技術外，在系統開發過程中仍然必須一如既往地實施其他種手段。除了使用形式化說明技術外，在系統開發過程中仍然必須一如既往地實施其他質量保證活動。質量保證活動。(8) 不應該盲目依賴形式化方法。不應該盲目依賴形式化方法。 形式化方法只不過是眾多工具中的一種。形式化方法只不過是眾多工具中的一種。 形式化方法并不能保證開發出的軟件絕對正確，形式化方法并不能保證開發出的軟件絕對正確， 例如：無法用形式化方法證明從非形式化需求到形式化規格說明的轉換是正確例如：無法用形式化方法證明從非形式化需求到形式化規格說明的轉換是正確的，因此，必須用其他方法

12、的，因此，必須用其他方法(例如，評審、測試例如，評審、測試)來驗證軟件正確性。來驗證軟件正確性。(9) 應該測試、測試再測試。應該測試、測試再測試。 形式化方法不僅不能保證軟件系統絕對正確，也不能證明系統性能或其他質量指標形式化方法不僅不能保證軟件系統絕對正確，也不能證明系統性能或其他質量指標符合需要，因此，軟件測試的重要性并沒有降低。符合需要，因此，軟件測試的重要性并沒有降低。(10) 應該重用。應該重用。 即使采用了形式化方法，軟件重用仍然是降低軟件成本和提高軟件質量的惟一合理的即使采用了形式化方法，軟件重用仍然是降低軟件成本和提高軟件質量的惟一合理的方法。而且用形式化方法說明的軟件構件具

13、有清晰定義的功能和接口，使得它們有更好方法。而且用形式化方法說明的軟件構件具有清晰定義的功能和接口，使得它們有更好的可重用性。的可重用性。 下面通過一個簡單例子介紹有窮狀態機的基本概念。下面通過一個簡單例子介紹有窮狀態機的基本概念。 一個保險箱上裝了一個復合鎖，鎖有三個位置，分別標記為一個保險箱上裝了一個復合鎖，鎖有三個位置，分別標記為1、2、3，轉盤可向左，轉盤可向左(L)或向右或向右(R)轉動。這樣，在任意時刻轉盤都有轉動。這樣，在任意時刻轉盤都有6種可能的運動，即種可能的運動，即1L、1R、2L、2R、3L和和3R。保險箱的組合密碼是。保險箱的組合密碼是1L、3R、2L，轉盤的任何其他運

14、動都將引起報警。圖，轉盤的任何其他運動都將引起報警。圖4.1描描繪了保險箱的狀態轉換情況。繪了保險箱的狀態轉換情況。4.2 有窮狀態機有窮狀態機 4.2.1 概念概念圖圖4.1 保險箱的狀態轉換圖保險箱的狀態轉換圖 圖圖4.1是一個有窮狀態機的狀態轉換圖。狀態轉換并不一定要用圖形方式描述，表是一個有窮狀態機的狀態轉換圖。狀態轉換并不一定要用圖形方式描述，表4.1（見書（見書68頁）的表格形式也可以表達同樣的信息。頁）的表格形式也可以表達同樣的信息。 說明：一個有窮狀態機包括下述說明：一個有窮狀態機包括下述5個部分：狀態集個部分：狀態集J、輸入集、輸入集K、由當前狀態和當前輸、由當前狀態和當前輸

15、入確定下一個狀態入確定下一個狀態(次態次態)的轉換函數的轉換函數T、初始態、初始態S和終態集和終態集F。對于保險箱的例子，相應的。對于保險箱的例子，相應的有窮狀態機的各部分如下。有窮狀態機的各部分如下。狀態集狀態集J：保險箱鎖定，：保險箱鎖定，A，B，保險箱解鎖，報警。，保險箱解鎖，報警。輸入集輸入集K：1L，1R，2L，2R，3L，3R。轉換函數轉換函數T：如表：如表4.1所示。所示。初始態初始態S：保險箱鎖定。：保險箱鎖定。終態集終態集F：保險箱解鎖，報警。：保險箱解鎖，報警。如果使用更形式化的術語，一個有窮狀態機可以表示為一個如果使用更形式化的術語，一個有窮狀態機可以表示為一個5元組元組

16、(J，K，T，S，F)，其，其中：中：J是一個有窮的非空狀態集；是一個有窮的非空狀態集；K是一個有窮的非空輸入集；是一個有窮的非空輸入集；T是一個從是一個從(J-F)K到到J的轉換函數；的轉換函數；SJ，是一個初始狀態；，是一個初始狀態；FJ，是終態集。，是終態集。 （1）有窮狀態機的應用）有窮狀態機的應用 例如，每個菜單驅動的用戶界面都是一個有窮狀態機的實現。一個菜單的顯示和一個例如，每個菜單驅動的用戶界面都是一個有窮狀態機的實現。一個菜單的顯示和一個狀態相對應，鍵盤輸入或用鼠標選擇一個圖標是使系統進入其他狀態的一個事件。狀態狀態相對應，鍵盤輸入或用鼠標選擇一個圖標是使系統進入其他狀態的一個

17、事件。狀態的每個轉換都具有下面的形式：的每個轉換都具有下面的形式：當前狀態當前狀態菜單菜單+事件事件所選擇的項所選擇的項下個狀態。下個狀態。（2）擴展）擴展 為了對一個系統進行規格說明，通常都需要對有窮狀態機做一個很有用的擴展，即在為了對一個系統進行規格說明，通常都需要對有窮狀態機做一個很有用的擴展，即在前述的前述的5元組中加入第元組中加入第6個組件個組件謂詞集謂詞集P，從而把有窮狀態機擴展為一個，從而把有窮狀態機擴展為一個6元組，其中元組，其中每個謂詞都是系統全局狀態每個謂詞都是系統全局狀態Y的函數。轉換函數的函數。轉換函數T現在是一個從現在是一個從(J-F)KP到到J的函數。的函數。現在的

18、轉換規則形式如下：現在的轉換規則形式如下：當前狀態當前狀態菜單菜單+事件事件所選擇的項所選擇的項+謂詞謂詞下個狀態。下個狀態。 電梯系統的規格說明。首先給出用自然語言描述的對電梯系統的需求：電梯系統的規格說明。首先給出用自然語言描述的對電梯系統的需求： 在一幢在一幢m層的大廈中需要一套控制層的大廈中需要一套控制n部電梯的產品，要求這部電梯的產品，要求這n部電梯按照約束條件部電梯按照約束條件C1，C2和和C3在樓層間移動。在樓層間移動。C1：每部電梯內有：每部電梯內有m個按鈕，每個按鈕代表一個樓層。當按下一個按鈕時該按鈕指示燈個按鈕，每個按鈕代表一個樓層。當按下一個按鈕時該按鈕指示燈亮，同時電梯

19、駛向相應的樓層，到達按鈕指定的樓層時指示燈熄滅。亮，同時電梯駛向相應的樓層，到達按鈕指定的樓層時指示燈熄滅。4.2.2 例子例子C2：除了大廈的最低層和最高層之外，每層樓都有兩個按鈕分別請求電梯上行和下行。：除了大廈的最低層和最高層之外，每層樓都有兩個按鈕分別請求電梯上行和下行。這兩個按鈕之一被按下時相應的指示燈亮，當電梯到達此樓層時燈熄滅，電梯向要求的這兩個按鈕之一被按下時相應的指示燈亮，當電梯到達此樓層時燈熄滅，電梯向要求的方向移動。方向移動。C3：當對電梯沒有請求時，它關門并停在當前樓層。：當對電梯沒有請求時，它關門并停在當前樓層。擴展的有窮狀態機的規格說明擴展的有窮狀態機的規格說明分析

20、分析 ：問題中有兩個按鈕集。問題中有兩個按鈕集。 n部電梯中的每一部都有部電梯中的每一部都有m個按鈕，一個按鈕對應一個樓層。因為這個按鈕，一個按鈕對應一個樓層。因為這mn個按鈕個按鈕都在電梯中，所以稱它們為電梯按鈕。都在電梯中，所以稱它們為電梯按鈕。 每層樓有兩個按鈕，一個請求向上，另一個請求向下，這些按鈕稱為樓層按鈕。每層樓有兩個按鈕，一個請求向上，另一個請求向下，這些按鈕稱為樓層按鈕。（1）電梯按鈕的狀態轉換（圖）電梯按鈕的狀態轉換（圖4.2） 令令EB(e,f)表示按下電梯表示按下電梯e內的按鈕并請求到內的按鈕并請求到f層去。層去。EB(e,f)有兩個狀態，分別是按鈕發有兩個狀態，分別是

21、按鈕發光光(打開打開)和不發光和不發光(關閉關閉)。 狀態是：狀態是： EBON(e,f)：電梯按鈕：電梯按鈕(e,f)打開打開 EBOFF(e,f)：電梯按鈕：電梯按鈕(e,f)關閉關閉 如果電梯按鈕如果電梯按鈕(e,f)發光且電梯到達發光且電梯到達f層，該按鈕將熄滅。層，該按鈕將熄滅。相反如果按鈕熄滅，則按下它時，按鈕將發光。相反如果按鈕熄滅，則按下它時，按鈕將發光。上述描述中包含了兩個事件，它們分別是：上述描述中包含了兩個事件，它們分別是：EBP(e,f)：電梯按鈕：電梯按鈕(e,f)被按下被按下EAF(e,f)：電梯：電梯e到達到達f層層圖圖4.2 電梯按鈕的狀態轉換圖電梯按鈕的狀態轉

22、換圖圖圖4.3樓層按鈕的狀態轉換圖樓層按鈕的狀態轉換圖 為了定義與這些事件和狀態相聯系的狀態轉換規則，需要一個謂詞為了定義與這些事件和狀態相聯系的狀態轉換規則，需要一個謂詞V(e,f)，它的含義，它的含義如下：如下： V(e,f)：電梯：電梯e停在停在f層層 如果電梯按鈕如果電梯按鈕(e,f)處于關閉狀態處于關閉狀態當前狀態當前狀態，而且電梯按鈕，而且電梯按鈕(e,f)被按下被按下事件事件，而，而且電梯且電梯e不在不在f層層謂詞謂詞，則該電梯按鈕打開發光，則該電梯按鈕打開發光下個狀態下個狀態。狀態轉換規則的形式化描述如下：狀態轉換規則的形式化描述如下：EBOFF(e,f)+EBP(e,f)+n

23、ot V(e,f)EBON(e,f)反之，如果電梯到達反之，如果電梯到達f層，而且電梯按鈕是打開的，于是它就會熄滅。這條轉換規則層，而且電梯按鈕是打開的，于是它就會熄滅。這條轉換規則可以形式化地表示為：可以形式化地表示為：EBON(e,f)+EAF(e,f)EBOFF(e,f)（2）樓層按鈕。）樓層按鈕。 令令FB(d,f)表示表示f層請求電梯向層請求電梯向d方向運動的按鈕（圖方向運動的按鈕（圖4.3） 樓層按鈕的狀態如下：樓層按鈕的狀態如下： FBON(d,f)：樓層按鈕：樓層按鈕(d,f)打開打開 FBOFF(d,f)：樓層按鈕：樓層按鈕(d,f)關閉關閉 如果樓層按鈕已經打開，而且一部電

24、梯到達如果樓層按鈕已經打開，而且一部電梯到達f層，則按鈕關閉。反之，如果樓層按鈕層，則按鈕關閉。反之，如果樓層按鈕原來是關閉的，被按下后該按鈕將打開。這段敘述中包含了以下兩個事件。原來是關閉的，被按下后該按鈕將打開。這段敘述中包含了以下兩個事件。 FBP(d,f)：樓層按鈕：樓層按鈕(d,f)被按下被按下 EAF(1n,f)：電梯：電梯1或或或或n到達到達f層層 其中其中1n表示或為表示或為1或為或為2或為或為n。 為了定義與這些事件和狀態相聯系的狀態轉換規則，同樣也需要一個謂詞，它是為了定義與這些事件和狀態相聯系的狀態轉換規則，同樣也需要一個謂詞，它是S(d,e,f)，它的定義如下。，它的定

25、義如下。 S(d,e,f)：電梯：電梯e停在停在f層并且移動方向由層并且移動方向由d確定為向上確定為向上(d=U)或向下或向下(d=D)或待定或待定(d=N)。 這個謂詞實際上是一個狀態，形式化方法允許把事件和狀態作為謂詞對待。這個謂詞實際上是一個狀態，形式化方法允許把事件和狀態作為謂詞對待。使用謂詞使用謂詞S(d,e,f)，形式化轉換規則為：，形式化轉換規則為：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=U or D。 如果在如果在f層請求電梯向層請求電梯向

26、d方向運動的樓層按鈕處于關閉狀態，現在該按鈕被按下，并且方向運動的樓層按鈕處于關閉狀態，現在該按鈕被按下，并且當時沒有正停在當時沒有正停在f層準備向層準備向d方向移動的電梯，則該樓層按鈕打開。反之，如果樓層按鈕方向移動的電梯，則該樓層按鈕打開。反之，如果樓層按鈕已經打開，且至少有一部電梯到達已經打開，且至少有一部電梯到達f層，該部電梯將朝層，該部電梯將朝d方向運動，則按鈕將關閉。方向運動，則按鈕將關閉。 在討論電梯按鈕狀態轉換規則時定義的謂詞在討論電梯按鈕狀態轉換規則時定義的謂詞V(e,f)，可以用謂詞，可以用謂詞S(d,e,f)重新定義如下：重新定義如下： V(e,f)=S(U,e,f)or

27、 S(D,e,f)or S(N,e,f) 定義電梯按鈕和樓層按鈕的狀態都是很簡單、直觀的事情。定義電梯按鈕和樓層按鈕的狀態都是很簡單、直觀的事情。（3）電梯的狀態及其轉換規則）電梯的狀態及其轉換規則 電梯狀態比較復雜。一個電梯狀態實質上包含許多子狀態。電梯狀態比較復雜。一個電梯狀態實質上包含許多子狀態。下面定義電梯的下面定義電梯的3個狀態：個狀態：M(d,e,f)：電梯：電梯e正沿正沿d方向移動，即將到達的是第方向移動，即將到達的是第f層層S(d,e,f)：電梯：電梯e停在停在f層，將朝層，將朝d方向移動方向移動(尚未關門尚未關門)W(e,f)：電梯：電梯e在在f層等待層等待(已關門已關門)

28、圖圖4.4是電梯的狀態轉換圖。是電梯的狀態轉換圖。3個電梯狀態個電梯狀態S(U,e,f)、S(N,e,f)和和S(D,e,f)已被組合成一個已被組合成一個大的狀態，這樣做的目的是減少狀態總數以簡化流圖。大的狀態，這樣做的目的是減少狀態總數以簡化流圖。 圖圖4.4中包含了下述中包含了下述3個可觸發狀態發生改變的事件。個可觸發狀態發生改變的事件。 DC(e,f)：電梯：電梯e在樓層在樓層f關上門關上門 ST(e,f)：電梯：電梯e靠近靠近f層時觸發傳感器，電梯控制器決定在當前樓層電梯是否停下層時觸發傳感器，電梯控制器決定在當前樓層電梯是否停下 RL：電梯按鈕或樓層按鈕被按下進入打開狀態，登錄需求：

29、電梯按鈕或樓層按鈕被按下進入打開狀態，登錄需求圖圖4.4 電梯的狀態轉換圖電梯的狀態轉換圖最后，給出電梯的狀態轉換規則。為簡單起見，這里給出的規則僅發生在關門之時。最后，給出電梯的狀態轉換規則。為簡單起見，這里給出的規則僅發生在關門之時。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) 第一條規則表明，如果電梯第一條規則表明，如果電梯e停在停在f層準備向上移動，且門已經關閉，則電梯將向上一層準備向上移動，且門已經關閉，則電梯將向上一樓層移動。樓層移動。 第二條和第三條規則，分別對應于電梯即將下降

30、或者沒有待處理的請求的情況。第二條和第三條規則，分別對應于電梯即將下降或者沒有待處理的請求的情況。 有窮狀態機方法采用了一種簡單的格式來描述規格說明：有窮狀態機方法采用了一種簡單的格式來描述規格說明：當前狀態當前狀態+事件事件+謂詞謂詞下個狀態下個狀態 這種形式的規格說明易于書寫、易于驗證，而且可以比較容易地把它轉變成設計或程這種形式的規格說明易于書寫、易于驗證，而且可以比較容易地把它轉變成設計或程序代碼。序代碼。 可以開發一個可以開發一個CASE工具把一個有窮狀態機規格說明直接轉變為源代碼。維護可以通工具把一個有窮狀態機規格說明直接轉變為源代碼。維護可以通過重新轉變來實現，也就是說，如果需要

31、一個新的狀態或事件，首先修改規格說明，然過重新轉變來實現，也就是說，如果需要一個新的狀態或事件，首先修改規格說明，然后直接由新的規格說明生成新版本的產品。后直接由新的規格說明生成新版本的產品。4.2.3 評價評價 有窮狀態機方法比數據流圖技術更精確，而且和它一樣易于理解。有窮狀態機方法比數據流圖技術更精確，而且和它一樣易于理解。 缺點：在開發一個大系統時三元組缺點：在開發一個大系統時三元組(即狀態、事件、謂詞即狀態、事件、謂詞)的數量會迅速增長。的數量會迅速增長。 此外，和數據流圖方法一樣，形式化的有窮狀態機方法也沒有處理定時需求。此外，和數據流圖方法一樣，形式化的有窮狀態機方法也沒有處理定時

32、需求。 下節將介紹的下節將介紹的Petri網技術，是一種可處理定時問題的形式化方法。網技術，是一種可處理定時問題的形式化方法。 （1）并發系統中遇到的一個主要問題是定時問題。）并發系統中遇到的一個主要問題是定時問題。 （2）如同步問題、競爭條件以及死鎖問題。）如同步問題、競爭條件以及死鎖問題。 （3）定時問題通常是由不好的設計或有錯誤的實現引起的。）定時問題通常是由不好的設計或有錯誤的實現引起的。 （4）用于確定系統中隱含的定時問題的一種有效技術是）用于確定系統中隱含的定時問題的一種有效技術是Petri網，這種技術的一個很網，這種技術的一個很大的優點是它也可以用于設計中。大的優點是它也可以用于

33、設計中。4.3 Petri網網 4.3.1 概念概念 Petri網是由網是由Carl Adam Petri發明的。最初只有自動化專家對發明的。最初只有自動化專家對Petri網感興趣，后來網感興趣，后來Petri網在計算機科學中也得到廣泛的應用，例如，在性能評價、操作系統和軟件工程等網在計算機科學中也得到廣泛的應用，例如，在性能評價、操作系統和軟件工程等領域，領域，Petri網應用得都比較廣泛。特別是已經證明，用網應用得都比較廣泛。特別是已經證明，用Petri網可以有效地描述并發活動。網可以有效地描述并發活動。 Petri網包含網包含4種元素：一組位置種元素：一組位置P、一組轉換、一組轉換T、輸

34、入函數、輸入函數I以及輸出函數以及輸出函數O。圖。圖4.5舉舉例說明了例說明了Petri網的組成。網的組成。圖圖4.5 Petri網的組成網的組成一組位置一組位置P為為P1，P2，P3，P4，在圖中用圓圈代表位置。，在圖中用圓圈代表位置。一組轉換一組轉換T為為t1，t2，在圖中用短直線表示轉換。，在圖中用短直線表示轉換。 兩個用于轉換的輸入函數，用由位置指向轉換的箭頭表示，它們是：兩個用于轉換的輸入函數，用由位置指向轉換的箭頭表示，它們是： I(t1)=P2，P4 I(t2)=P2 兩個用于轉換的輸出函數，用由轉換指向位置的箭頭表示，它們是：兩個用于轉換的輸出函數，用由轉換指向位置的箭頭表示，

35、它們是： O(t1)=P1 O(t2)=P3，P3注意，輸出函數注意，輸出函數O(t2)中有兩個中有兩個P3，是因為有兩個箭頭由，是因為有兩個箭頭由t2指向指向P3。更形式化的更形式化的Petri網結構，是一個四元組網結構，是一個四元組C=(P,T,I,O)。其中，其中，P=P1，Pn是一個有窮位置集，是一個有窮位置集，n0。T=t1，tm是一個有窮轉換集，是一個有窮轉換集，m0，且，且T和和P不相交。不相交。I：TP為輸入函數，是由轉換到位置無序單位組為輸入函數，是由轉換到位置無序單位組(bags)的映射。的映射。O：TP為輸出函數，是由轉換到位置無序單位組的映射。為輸出函數，是由轉換到位置

36、無序單位組的映射。 一個無序單位組或多重組是允許一個元素有多個實例的廣義集。一個無序單位組或多重組是允許一個元素有多個實例的廣義集。 Petri網的標記是在網的標記是在Petri網中權標網中權標(token)的分配。的分配。 例如，在圖例如，在圖4.6中有中有4個權標，其中一個在個權標，其中一個在P1中，兩個在中，兩個在P2中，中，P3中沒有，還有一個在中沒有，還有一個在P4中。上述標記可以用向量中。上述標記可以用向量(1，2，0，1)表示。表示。 由于由于P2和和P4中有權標，因此中有權標，因此t1啟動啟動(即被激發即被激發)。通常，當每個輸入位置所擁有的權標。通常，當每個輸入位置所擁有的權

37、標數大于等于從該位置到轉換的線數時，就允許轉換。數大于等于從該位置到轉換的線數時，就允許轉換。 當當t1被激發時，被激發時，P2和和P4上各有一個權標被移出，而上各有一個權標被移出，而P1上則增加一個權標。上則增加一個權標。Petri網中權標總數不是固定的，在這個例子中兩個權標被移出，而網中權標總數不是固定的，在這個例子中兩個權標被移出，而P1上只能增加一個權上只能增加一個權標。標。 在圖在圖4.6中中P2上有權標，因此上有權標，因此t2也可以被激發。當也可以被激發。當t2被激發時，被激發時，P2上將移走一個上將移走一個權標，而權標，而P3上新增加兩個權標。上新增加兩個權標。 Petri網具有

38、非確定性，也就是說，如果數個轉換都達到了激發條件，則其中任意一個網具有非確定性，也就是說，如果數個轉換都達到了激發條件，則其中任意一個都可以被激發。圖都可以被激發。圖4.6所示所示Petri網的標記為網的標記為(1，2，0，1)，t1和和t2都可以被激發。假設都可以被激發。假設t1被被激發了，則結果如圖激發了，則結果如圖4.7所示，標記為所示，標記為(2，1，0，0)。此時，只有。此時，只有t2可以被激發。如果可以被激發。如果t2也也被激發了，則權標從被激發了，則權標從P2中移出，兩個新權標被放在中移出，兩個新權標被放在P3上，結果如圖上，結果如圖4.8所示，標記為所示，標記為(2，0，2，0

39、)。圖圖4.6 帶標記的帶標記的Petri網網圖圖4.7 圖圖4.6的的Petri網在轉換網在轉換 t1被激發后的情況被激發后的情況圖圖4.8 圖圖4.7的的Petri網在轉換網在轉換 t2被激發后的情況被激發后的情況圖圖4.9 含禁止線的含禁止線的Petri網網加入禁止線加入禁止線（1）禁止線是用一個小圓圈表示的輸入線。）禁止線是用一個小圓圈表示的輸入線。（2）當每個輸入線上至少有一個權標，而禁止線上沒有權標時，相應的轉換才是）當每個輸入線上至少有一個權標，而禁止線上沒有權標時，相應的轉換才是允許的。允許的。在圖在圖4.9中，中，P3上有一個權標而上有一個權標而P2上沒有權標，因此轉換上沒有

40、權標，因此轉換t1可以被激發。可以被激發。 更形式化地說，更形式化地說，Petri網網C=(P，T，I，O，M)中的標記中的標記M，是由一組位置，是由一組位置P到一組非負到一組非負整數的映射：整數的映射： M：P0，1，2， 這樣，帶有標記的這樣，帶有標記的Petri網成為一個五元組網成為一個五元組(P，T，I，O，M)。 把把Petri網應用于上一節討論過的電梯問題。當用網應用于上一節討論過的電梯問題。當用Petri網表示電梯系統的規格說明時，網表示電梯系統的規格說明時，每個樓層用一個位置每個樓層用一個位置Ff代表代表(1fm)，在，在Petri網中電梯是用一個權標代表的。在位置網中電梯是用

41、一個權標代表的。在位置Ff上上有權標，表示在樓層有權標，表示在樓層f上有電梯。上有電梯。1. 電梯按鈕電梯按鈕電梯問題的第一個約束條件描述了電梯按鈕的行為，現在復述一下這個約束條件。電梯問題的第一個約束條件描述了電梯按鈕的行為，現在復述一下這個約束條件。4.3.2 例子例子第一條約束第一條約束C1： （1）每部電梯有）每部電梯有m個按鈕，每層對應一個按鈕。個按鈕，每層對應一個按鈕。 （2）當按下一個按鈕時該按鈕指示燈亮，指示電梯移往相應的樓層。）當按下一個按鈕時該按鈕指示燈亮，指示電梯移往相應的樓層。 （3）當電梯到達指定的樓層時，按鈕將熄滅。）當電梯到達指定的樓層時，按鈕將熄滅。 （4）電梯

42、中樓層）電梯中樓層f的按鈕，在的按鈕，在Petri網中用位置網中用位置EBf表示表示(1fm)。在。在EBf上有一個權標，上有一個權標，就表示電梯內樓層就表示電梯內樓層f的按鈕被按下了。的按鈕被按下了。說明：說明： 電梯按鈕只有在第一次被按下時才會由暗變亮，以后再按它則只會被忽略。電梯按鈕只有在第一次被按下時才會由暗變亮，以后再按它則只會被忽略。 電梯按鈕的行為規律（圖電梯按鈕的行為規律（圖4.10）。）。（1）假設按鈕沒有發亮，顯然在位置）假設按鈕沒有發亮，顯然在位置EBf上沒有權標，從而在存在禁止線的情況下，轉上沒有權標，從而在存在禁止線的情況下，轉換換“EBf被按下被按下”是允許發生的。

43、是允許發生的。 假設現在按下按鈕，則轉換被激發并在假設現在按下按鈕，則轉換被激發并在EBf上放置了一個權標，如圖上放置了一個權標，如圖4.10所示。所示。以后不論再按下多少次按鈕，禁止線與現有權標的組合都決定了轉換以后不論再按下多少次按鈕，禁止線與現有權標的組合都決定了轉換“EBf被按下被按下”不能再被激發了，因此，位置不能再被激發了，因此，位置EBf上的權標數不會多于上的權標數不會多于1。圖圖4.10 Petri網表示的電梯按鈕網表示的電梯按鈕（2）假設電梯由）假設電梯由g層駛向層駛向f層，因為電梯在層，因為電梯在g層，如圖層，如圖4.10所示，位置所示，位置Fg上有一個權標。由上有一個權標

44、。由于每條輸入線上各有一個權標，轉換于每條輸入線上各有一個權標，轉換“電梯在運行電梯在運行”被激發，從而被激發，從而EBf和和Fg上的權標被上的權標被移走，按鈕移走，按鈕EBf被關閉，在位置被關閉，在位置Ff上出現一個新權標，即轉換的激發使電梯由上出現一個新權標，即轉換的激發使電梯由g層駛到層駛到f層。層。說明：說明： 電梯由電梯由g層移到層移到f層是需要時間的，為處理這個情況及其他類似的問題層是需要時間的，為處理這個情況及其他類似的問題(例如，由例如，由于物理上的原因按鈕被按下后不能馬上發亮于物理上的原因按鈕被按下后不能馬上發亮)，Petri網模型中必須加入時限。也就是網模型中必須加入時限。

45、也就是說，在標準說，在標準Petri網中轉換是瞬時完成的，而在現實情況下就需要時間控制網中轉換是瞬時完成的，而在現實情況下就需要時間控制Petri網，網，以使轉換與非零時間相聯系。以使轉換與非零時間相聯系。2. 樓層按鈕樓層按鈕在第二個約束條件中描述了樓層按鈕的行為。在第二個約束條件中描述了樓層按鈕的行為。第二條約束第二條約束C2：除了第一層與頂層之外，每個樓層都有兩個按鈕，一個要求電梯上行，：除了第一層與頂層之外，每個樓層都有兩個按鈕，一個要求電梯上行，另一個要求電梯下行。這些按鈕在按下時發亮，當電梯到達該層并將向指定方向移動時，另一個要求電梯下行。這些按鈕在按下時發亮，當電梯到達該層并將向

46、指定方向移動時，相應的按鈕才會熄滅。相應的按鈕才會熄滅。在在Petri網中樓層按鈕用位置網中樓層按鈕用位置FBfu和和FBfd表示，分別代表表示，分別代表f樓層請求電梯上行和下行的按鈕。樓層請求電梯上行和下行的按鈕。底層的按鈕為底層的按鈕為FB1u，最高層的按鈕為，最高層的按鈕為FBmd，中間每一層有兩個按鈕，中間每一層有兩個按鈕FBfu和和FBfd(1fm)。圖圖4.11 Petri網表示樓層按鈕網表示樓層按鈕 圖圖4.11所示的情況為電梯由所示的情況為電梯由g層駛向層駛向f層。根據電梯乘客的要求，某一個樓層按鈕亮或層。根據電梯乘客的要求，某一個樓層按鈕亮或兩個樓層按鈕都亮。如果兩個按鈕都亮

47、了，則只有一個按鈕熄滅。圖兩個樓層按鈕都亮。如果兩個按鈕都亮了，則只有一個按鈕熄滅。圖4.11所示的所示的Petri網網可以保證，當兩個按鈕都亮了的時候，只有一個按鈕熄滅。但是要保證按鈕熄滅正確，可以保證，當兩個按鈕都亮了的時候，只有一個按鈕熄滅。但是要保證按鈕熄滅正確，則需要更復雜的則需要更復雜的Petri網模型。網模型。第三條約束。第三條約束。第三條約束第三條約束C3：當電梯沒有收到請求時，它將停留在當前樓層并關門。：當電梯沒有收到請求時，它將停留在當前樓層并關門。這條約束很容易實現，如圖這條約束很容易實現，如圖4.11所示，當沒有請求所示，當沒有請求(FBfu和和FBfd上無權標）時，任

48、何上無權標）時，任何一個轉換一個轉換“電梯在運行電梯在運行”都不能被激發。都不能被激發。 用用Z語言描述的、最簡單的形式化規格說明含有下述語言描述的、最簡單的形式化規格說明含有下述4個部分：個部分：給定的集合、數據類型及常數。給定的集合、數據類型及常數。狀態定義。狀態定義。初始狀態。初始狀態。操作。操作。4.4 Z語言語言 4.4.1 簡介簡介1. 給定的集合給定的集合一個一個Z規格說明從一系列給定的初始化集合開始。所謂初始化集合就是不需要詳細定義的規格說明從一系列給定的初始化集合開始。所謂初始化集合就是不需要詳細定義的集合，這種集合用帶方括號的形式表示。對于電梯問題，給定的初始化集合稱為集合

49、，這種集合用帶方括號的形式表示。對于電梯問題，給定的初始化集合稱為Button，即所有按鈕的集合，因此，即所有按鈕的集合，因此，Z規格說明開始于：規格說明開始于：Button2. 狀態定義狀態定義一個一個Z規格說明由若干個規格說明由若干個“格格(schema)”組成，每個格含有一組變量說明和一系列限定變組成，每個格含有一組變量說明和一系列限定變量取值范圍的謂詞。例如，格量取值范圍的謂詞。例如，格S的格式如圖的格式如圖4.12所示。所示。圖圖4.12 Z格格S的格式的格式在電梯問題中，在電梯問題中，Button有有4個子集，即個子集，即floor_buttons(樓層按鈕的集合樓層按鈕的集合)、

50、elevator_buttons(電梯按鈕的集合電梯按鈕的集合)、buttons(電梯問題中所有按鈕的集合電梯問題中所有按鈕的集合)以及以及pushed(所所有被按的按鈕的集合，即所有處于打開狀態的按鈕的集合有被按的按鈕的集合，即所有處于打開狀態的按鈕的集合)。圖。圖4.13（見書（見書76頁）描述了頁）描述了格格Button_State，其中，符號，其中，符號P表示冪集表示冪集(即給定集的所有子集即給定集的所有子集)。約束條件聲明，。約束條件聲明，floor_buttons集與集與elevator_buttons集不相交，而且它們共同組成集不相交，而且它們共同組成buttons集集(在下面的

51、討論在下面的討論中并不需要中并不需要floor_buttons集和集和elevator_buttons集，把它們放于圖集，把它們放于圖4.13中只是用來說明中只是用來說明Z格格包含的內容包含的內容)。3. 初始狀態初始狀態抽象的初始狀態是指系統第一次開啟時的狀態。對于電梯問題來說，抽象的初始狀態為：抽象的初始狀態是指系統第一次開啟時的狀態。對于電梯問題來說，抽象的初始狀態為：Button_InitButton_Statepushed=上式表示，當系統首次開啟時上式表示，當系統首次開啟時pushed集為空，即所有按鈕都處于關閉狀態。集為空，即所有按鈕都處于關閉狀態。4. 操作操作如果一個原來處于

52、關閉狀態的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到如果一個原來處于關閉狀態的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到pushed集中。圖集中。圖4.14（見書（見書77頁）定義了操作頁）定義了操作Push_Button(按按鈕按按鈕)。 操作的謂詞部分，包含了一組調用操作的前置條件，以及操作完全結束后的后置條件。操作的謂詞部分，包含了一組調用操作的前置條件，以及操作完全結束后的后置條件。如果前置條件成立，則操作執行完成后可得到后置條件。但是，如果在前置條件不成立如果前置條件成立，則操作執行完成后可得到后置條件。但是，如果在前置條件不成立的情況下調用該操作，則不能得到指定的結果的情況下調

53、用該操作，則不能得到指定的結果(因此結果無法預測因此結果無法預測)。假設電梯到達了某樓層，如果相應的樓層按鈕已經打開，則此時它會關閉；同樣，如果假設電梯到達了某樓層，如果相應的樓層按鈕已經打開，則此時它會關閉；同樣，如果相應的電梯按鈕已經打開，則此時它也會關閉。也就是說，如果相應的電梯按鈕已經打開，則此時它也會關閉。也就是說，如果“button?”屬于屬于pushed集，則將它移出該集合，如圖集，則將它移出該集合，如圖4.15（見書（見書77頁）所示頁）所示(符號符號“”表示集合差運算表示集合差運算)。已經在許多軟件開發項目中成功地運用了已經在許多軟件開發項目中成功地運用了Z語言，目前，語言，

54、目前，Z也許是應用得最廣泛的形式化也許是應用得最廣泛的形式化語言，尤其是在大型項目中語言，尤其是在大型項目中Z語言的優勢更加明顯。語言的優勢更加明顯。Z語言之所以會獲得如此多的成功，語言之所以會獲得如此多的成功，主要有以下幾個原因：主要有以下幾個原因：(1) 可以比較容易地發現用可以比較容易地發現用Z寫的規格說明的錯誤，特別是在自己審查規格說明，及根據寫的規格說明的錯誤，特別是在自己審查規格說明，及根據形式化的規格說明來審查設計與代碼時，情況更是如此。形式化的規格說明來審查設計與代碼時，情況更是如此。(2) 用用Z寫規格說明時，要求作者十分精確地使用寫規格說明時，要求作者十分精確地使用Z說明符

55、。由于對精確性的要求很高，說明符。由于對精確性的要求很高，從而和非形式化規格說明相比，減少了模糊性、不一致性和遺漏。從而和非形式化規格說明相比，減少了模糊性、不一致性和遺漏。4.4.2 評價評價(3) Z是一種形式化語言，在需要時開發者可以嚴格地驗證規格說明的正確性。是一種形式化語言，在需要時開發者可以嚴格地驗證規格說明的正確性。(4) 雖然完全學會雖然完全學會Z語言相當困難，但是，經驗表明，只學過中學數學的軟件開發人員仍語言相當困難，但是，經驗表明，只學過中學數學的軟件開發人員仍然可以只用比較短的時間就學會編寫然可以只用比較短的時間就學會編寫Z規格說明，當然，這些人還沒有能力證明規格說明規格

56、說明，當然，這些人還沒有能力證明規格說明的結果是否正確。的結果是否正確。(5) 使用使用Z語言可以降低軟件開發費用。雖然用語言可以降低軟件開發費用。雖然用Z寫規格說明所需用的時間比使用非形式寫規格說明所需用的時間比使用非形式化技術要多，但開發過程所需要的總時間卻減少了。化技術要多，但開發過程所需要的總時間卻減少了。(6) 雖然用戶無法理解用雖然用戶無法理解用Z寫的規格說明，但是，可以依據寫的規格說明，但是，可以依據Z規格說明用自然語言重寫規規格說明用自然語言重寫規格說明。經驗證明，這樣得到的自然語言規格說明，比直接用自然語言寫出的非形式化格說明。經驗證明，這樣得到的自然語言規格說明，比直接用自

57、然語言寫出的非形式化規格說明更清楚、更正確。規格說明更清楚、更正確。使用形式化規格說明是全球的總趨勢，過去，主要是歐洲習慣于使用形式化規格說明技使用形式化規格說明是全球的總趨勢，過去，主要是歐洲習慣于使用形式化規格說明技術，現在越來越多的美國公司也開始使用形式化規格說明技術。術，現在越來越多的美國公司也開始使用形式化規格說明技術。基于數學的形式化規格說明技術，目前還沒有在軟件產業界廣泛應用，但是，與欠形式基于數學的形式化規格說明技術，目前還沒有在軟件產業界廣泛應用，但是，與欠形式化的方法比較起來，它確實有實質性的優點：形式化的規格說明可以用數學方法研究、化的方法比較起來，它確實有實質性的優點：形式化的規格說明可以用數學方法研究、驗證驗證(例如，一個正確的程序可以被證明滿足其規格說明，兩個規格說明可以被證明是等例如，一個正確的程序可以被證明滿足其規格說明，兩個規格說明可以被證明是等價的，規格說明中存在的某些形式的不完整性和不一致性可以被自動地檢測出來價的，規格說明中存在的某些形式的不完整性和不一致性可以被自動地檢測出來)。此外，。此外，形式化的規格說明消除了二義性，而且它鼓勵軟