軟件工程第4章.

1、第第4章章 形式化說明技術(shù)形式化說明技術(shù)4.1 概述概述4.2 有窮狀態(tài)機有窮狀態(tài)機4.3 Petri網(wǎng)網(wǎng)4.4 Z語言語言4.5 小結(jié)小結(jié)習題習題按照形式化的程度，可以把軟件工程使用的方法劃按照形式化的程度，可以把軟件工程使用的方法劃分成非形式化、半形式化和形式化分成非形式化、半形式化和形式化3類。用自然語類。用自然語言描述需求規(guī)格說明，是典型的非形式化方法。用言描述需求規(guī)格說明，是典型的非形式化方法。用數(shù)據(jù)流圖或?qū)嶓w數(shù)據(jù)流圖或?qū)嶓w-聯(lián)系圖建立模型，是典型的半形聯(lián)系圖建立模型，是典型的半形式化方法。式化方法。所謂形式化方法，是描述系統(tǒng)性質(zhì)的基于數(shù)學的技所謂形式化方法，是描述系統(tǒng)性質(zhì)的基于數(shù)學

2、的技術(shù)，也就是說，如果一種方法有堅實的數(shù)學基礎(chǔ)，術(shù)，也就是說，如果一種方法有堅實的數(shù)學基礎(chǔ)，那么它就是形式化的。那么它就是形式化的。用自然語言書寫的系統(tǒng)規(guī)格說明書，可能存在矛盾、用自然語言書寫的系統(tǒng)規(guī)格說明書，可能存在矛盾、二義性、含糊性、不完整性及抽象層次混亂等問題。二義性、含糊性、不完整性及抽象層次混亂等問題。所謂矛盾是指一組相互沖突的陳述。所謂矛盾是指一組相互沖突的陳述。二義性是指讀者可以用不同方式理解的陳述。二義性是指讀者可以用不同方式理解的陳述。4.1 概述概述 4.1.1 非形式化方法的缺點非形式化方法的缺點系統(tǒng)規(guī)格說明書是很龐大的文檔，因此，幾乎不可系統(tǒng)規(guī)格說明書是很龐大的文檔，

3、因此，幾乎不可避免地會出現(xiàn)含糊性。實際上，這樣籠統(tǒng)的陳述并避免地會出現(xiàn)含糊性。實際上，這樣籠統(tǒng)的陳述并沒有給出任何有用的信息。沒有給出任何有用的信息。不完整性可能是在系統(tǒng)規(guī)格說明中最常遇到的問題不完整性可能是在系統(tǒng)規(guī)格說明中最常遇到的問題之一。之一。抽象層次混亂是指在非常抽象的陳述中混進了一些抽象層次混亂是指在非常抽象的陳述中混進了一些關(guān)于細節(jié)的低層次陳述。這樣的規(guī)格說明書使得讀關(guān)于細節(jié)的低層次陳述。這樣的規(guī)格說明書使得讀者很難了解系統(tǒng)的整體功能結(jié)構(gòu)。者很難了解系統(tǒng)的整體功能結(jié)構(gòu)。人在理解用自然語言描述的規(guī)格說明時，容易產(chǎn)生人在理解用自然語言描述的規(guī)格說明時，容易產(chǎn)生二義性。為了克服非形式化方

4、法的缺點，人們把數(shù)二義性。為了克服非形式化方法的缺點，人們把數(shù)學引入軟件開發(fā)過程，創(chuàng)造了基于數(shù)學的形式化方學引入軟件開發(fā)過程，創(chuàng)造了基于數(shù)學的形式化方法。法。在開發(fā)大型軟件系統(tǒng)的過程中應用數(shù)學，能夠帶來在開發(fā)大型軟件系統(tǒng)的過程中應用數(shù)學，能夠帶來下述的幾個優(yōu)點：下述的幾個優(yōu)點：數(shù)學最有用的一個性質(zhì)是，它能夠簡潔準確地描述數(shù)學最有用的一個性質(zhì)是，它能夠簡潔準確地描述物理現(xiàn)象、對象或動作的結(jié)果，因此是理想的建模物理現(xiàn)象、對象或動作的結(jié)果，因此是理想的建模工具。數(shù)學特別適合于表示狀態(tài)，也就是表示工具。數(shù)學特別適合于表示狀態(tài)，也就是表示“做做什么什么”。4.1.2 形式化方法的優(yōu)點形式化方法的優(yōu)點需求

5、規(guī)格說明書主要描述應用系統(tǒng)在運行前和運行需求規(guī)格說明書主要描述應用系統(tǒng)在運行前和運行后的狀態(tài)，因此，數(shù)學比自然語言更適于描述詳細后的狀態(tài)，因此，數(shù)學比自然語言更適于描述詳細的需求。在理想情況下，分析員可以寫出系統(tǒng)的數(shù)的需求。在理想情況下，分析員可以寫出系統(tǒng)的數(shù)學規(guī)格說明，它準確到幾乎沒有二義性，而且可以學規(guī)格說明，它準確到幾乎沒有二義性，而且可以用數(shù)學方法來驗證，以發(fā)現(xiàn)存在的矛盾和不完整性，用數(shù)學方法來驗證，以發(fā)現(xiàn)存在的矛盾和不完整性，在這樣的規(guī)格說明中完全沒有含糊性。但是，實際在這樣的規(guī)格說明中完全沒有含糊性。但是，實際情況并不這么簡單，軟件系統(tǒng)的復雜性是出了名的，情況并不這么簡單，軟件系統(tǒng)

6、的復雜性是出了名的，希望用少數(shù)幾個數(shù)學公式來描述它，是根本不可能希望用少數(shù)幾個數(shù)學公式來描述它，是根本不可能的。此外，即使應用了形式化方法，完整性也是難的。此外，即使應用了形式化方法，完整性也是難于保證的：由于溝通不夠，可能遺漏了客戶的一些于保證的：由于溝通不夠，可能遺漏了客戶的一些需求；規(guī)格說明的撰寫者可能有意省略了系統(tǒng)的某需求；規(guī)格說明的撰寫者可能有意省略了系統(tǒng)的某些特征，以便設(shè)計者在選擇實現(xiàn)方法時有一定自由些特征，以便設(shè)計者在選擇實現(xiàn)方法時有一定自由度；要設(shè)想出使用一個大型復雜系統(tǒng)的每一個可能度；要設(shè)想出使用一個大型復雜系統(tǒng)的每一個可能的情景，通常是做不到的。的情景，通常是做不到的。在軟

7、件開發(fā)過程中使用數(shù)學的另一個優(yōu)點是，可以在軟件開發(fā)過程中使用數(shù)學的另一個優(yōu)點是，可以在不同的軟件工程活動之間平滑地過渡。不僅功能在不同的軟件工程活動之間平滑地過渡。不僅功能規(guī)格說明，而且系統(tǒng)設(shè)計也可以用數(shù)學表達，當然，規(guī)格說明，而且系統(tǒng)設(shè)計也可以用數(shù)學表達，當然，程序代碼也是一種數(shù)學符號程序代碼也是一種數(shù)學符號(雖然是一種相當繁瑣、雖然是一種相當繁瑣、冗長的數(shù)學符號冗長的數(shù)學符號)。數(shù)學作為軟件開發(fā)工具的最后一個優(yōu)點是，它提供數(shù)學作為軟件開發(fā)工具的最后一個優(yōu)點是，它提供了高層確認的手段。可以使用數(shù)學方法證明，設(shè)計了高層確認的手段?？梢允褂脭?shù)學方法證明，設(shè)計符合規(guī)格說明，程序代碼正確地實現(xiàn)了設(shè)計

8、結(jié)果。符合規(guī)格說明，程序代碼正確地實現(xiàn)了設(shè)計結(jié)果。人們對形式化方法的看法并不一致。形式化方法對人們對形式化方法的看法并不一致。形式化方法對某些軟件工程師很有吸引力，其擁護者甚至宣稱這某些軟件工程師很有吸引力，其擁護者甚至宣稱這種方法可以引發(fā)軟件開發(fā)方法的革命；另一些人則種方法可以引發(fā)軟件開發(fā)方法的革命；另一些人則對把數(shù)學引入軟件開發(fā)過程持懷疑甚至反對的態(tài)度。對把數(shù)學引入軟件開發(fā)過程持懷疑甚至反對的態(tài)度。編者認為，對形式化方法也應該編者認為，對形式化方法也應該“一分為二一分為二”，既，既不要過分夸大它的優(yōu)點也不要一概排斥。為了更好不要過分夸大它的優(yōu)點也不要一概排斥。為了更好地發(fā)揮這種方法的長處，

9、下面給出應用形式化方法地發(fā)揮這種方法的長處，下面給出應用形式化方法的幾條準則，供讀者在實際工作中使用。的幾條準則，供讀者在實際工作中使用。4.1.3 應用形式化方法的準則應用形式化方法的準則(1) 應該選用適當?shù)谋硎痉椒?。通常，一種規(guī)格說應該選用適當?shù)谋硎痉椒?。通常，一種規(guī)格說明技術(shù)只能用自然的方式說明某一類概念，如果用明技術(shù)只能用自然的方式說明某一類概念，如果用這種技術(shù)描述其不適于描述的概念，則不僅工作量這種技術(shù)描述其不適于描述的概念，則不僅工作量大而且描述方式也很復雜。因此，應該仔細選擇一大而且描述方式也很復雜。因此，應該仔細選擇一種適用于當前項目的形式化說明技術(shù)。種適用于當前項目的形式化

10、說明技術(shù)。(2) 應該形式化，但不要過分形式化。目前的形式應該形式化，但不要過分形式化。目前的形式化技術(shù)還不適于描述系統(tǒng)的每個方面。但是，也不化技術(shù)還不適于描述系統(tǒng)的每個方面。但是，也不能因此就認為完全沒必要采用形式化方法。形式化能因此就認為完全沒必要采用形式化方法。形式化規(guī)格說明技術(shù)要求我們非常準確地描述事物，因此規(guī)格說明技術(shù)要求我們非常準確地描述事物，因此有助于防止含糊和誤解。事實上，如果用形式化方有助于防止含糊和誤解。事實上，如果用形式化方法仔細說明系統(tǒng)中易出錯的或關(guān)鍵的部分，則只用法仔細說明系統(tǒng)中易出錯的或關(guān)鍵的部分，則只用適中的工作量就能獲得較大回報。適中的工作量就能獲得較大回報。(

11、3) 應該估算成本。為了使用形式化方法，通常需應該估算成本。為了使用形式化方法，通常需要事先進行大量的培訓。最好預先估算所需的成本要事先進行大量的培訓。最好預先估算所需的成本并編入預算。并編入預算。(4) 應該有形式化方法顧問隨時提供咨詢。絕大多應該有形式化方法顧問隨時提供咨詢。絕大多數(shù)軟件工程師對形式化方法中使用的數(shù)學和邏輯并數(shù)軟件工程師對形式化方法中使用的數(shù)學和邏輯并不很熟悉，而且沒受過使用形式化方法的專業(yè)訓練，不很熟悉，而且沒受過使用形式化方法的專業(yè)訓練，因此，需要專家指導和培訓。因此，需要專家指導和培訓。(5) 不應該放棄傳統(tǒng)的開發(fā)方法。把形式化方法和不應該放棄傳統(tǒng)的開發(fā)方法。把形式化

12、方法和結(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋硎强赡艿?，而結(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋硎强赡艿模矣捎谌￠L補短往往能獲得很好的效果。且由于取長補短往往能獲得很好的效果。(6) 應該建立詳盡的文檔。建議使用自然語言注釋應該建立詳盡的文檔。建議使用自然語言注釋形式化的規(guī)格說明書，以幫助用戶和維護人員理解形式化的規(guī)格說明書，以幫助用戶和維護人員理解系統(tǒng)。系統(tǒng)。(7) 不應該放棄質(zhì)量標準。形式化方法并不能保證不應該放棄質(zhì)量標準。形式化方法并不能保證軟件的正確性，它們只不過是有助于開發(fā)出高質(zhì)量軟件的正確性，它們只不過是有助于開發(fā)出高質(zhì)量軟件的一種手段。除了使用形式化說明技術(shù)外，在軟件的一種手段。除了使用形

13、式化說明技術(shù)外，在系統(tǒng)開發(fā)過程中仍然必須一如既往地實施其他質(zhì)量系統(tǒng)開發(fā)過程中仍然必須一如既往地實施其他質(zhì)量保證活動。保證活動。(8) 不應該盲目依賴形式化方法。這種方法不是包不應該盲目依賴形式化方法。這種方法不是包治百病的靈丹妙藥，它們只不過是眾多工具中的一治百病的靈丹妙藥，它們只不過是眾多工具中的一種。形式化方法并不能保證開發(fā)出的軟件絕對正確，種。形式化方法并不能保證開發(fā)出的軟件絕對正確，例如，無法用形式化方法證明從非形式化需求到形例如，無法用形式化方法證明從非形式化需求到形式化規(guī)格說明的轉(zhuǎn)換是正確的，因此，必須用其他式化規(guī)格說明的轉(zhuǎn)換是正確的，因此，必須用其他方法方法(例如，評審、測試例如

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

15、定義的功能和接口，使得它們有更好的可重用性。定義的功能和接口，使得它們有更好的可重用性。下面通過一個簡單例子介紹有窮狀態(tài)機的基本概念。下面通過一個簡單例子介紹有窮狀態(tài)機的基本概念。一個保險箱上裝了一個復合鎖，鎖有三個位置，分一個保險箱上裝了一個復合鎖，鎖有三個位置，分別標記為別標記為1、2、3，轉(zhuǎn)盤可向左，轉(zhuǎn)盤可向左(L)或向右或向右(R)轉(zhuǎn)動。轉(zhuǎn)動。這樣，在任意時刻轉(zhuǎn)盤都有這樣，在任意時刻轉(zhuǎn)盤都有6種可能的運動，即種可能的運動，即1L、1R、2L、2R、3L和和3R。保險箱的組合密碼是。保險箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤的任何其他運動都將引起報警。圖，轉(zhuǎn)盤的任何其他運動都將引起報警。圖

16、4.1描繪了保險箱的狀態(tài)轉(zhuǎn)換情況。描繪了保險箱的狀態(tài)轉(zhuǎn)換情況。4.2 有窮狀態(tài)機有窮狀態(tài)機 4.2.1 概念概念圖圖4.1 保險箱的狀態(tài)轉(zhuǎn)換圖保險箱的狀態(tài)轉(zhuǎn)換圖圖圖4.1是一個有窮狀態(tài)機的狀態(tài)轉(zhuǎn)換圖。狀態(tài)轉(zhuǎn)換是一個有窮狀態(tài)機的狀態(tài)轉(zhuǎn)換圖。狀態(tài)轉(zhuǎn)換并不一定要用圖形方式描述，表并不一定要用圖形方式描述，表4.1（見書（見書68頁）頁）的表格形式也可以表達同樣的信息。的表格形式也可以表達同樣的信息。從上面這個簡單例子可以看出，一個有窮狀態(tài)機包從上面這個簡單例子可以看出，一個有窮狀態(tài)機包括下述括下述5個部分：狀態(tài)集個部分：狀態(tài)集J、輸入集、輸入集K、由當前狀態(tài)、由當前狀態(tài)和當前輸入確定下一個狀態(tài)和當前

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

18、，F(xiàn))，其中：，其中：J是一個有窮的非空狀態(tài)集；是一個有窮的非空狀態(tài)集；K是一個有窮的非空輸入集；是一個有窮的非空輸入集；T是一個從是一個從(J-F)K到到J的轉(zhuǎn)換函數(shù)；的轉(zhuǎn)換函數(shù)；SJ，是一個初始狀態(tài)；，是一個初始狀態(tài)；FJ，是終態(tài)集。，是終態(tài)集。 有窮狀態(tài)機的概念在計算機系統(tǒng)中應用得非常廣泛。有窮狀態(tài)機的概念在計算機系統(tǒng)中應用得非常廣泛。例如，每個菜單驅(qū)動的用戶界面都是一個有窮狀態(tài)例如，每個菜單驅(qū)動的用戶界面都是一個有窮狀態(tài)機的實現(xiàn)。一個菜單的顯示和一個狀態(tài)相對應，鍵機的實現(xiàn)。一個菜單的顯示和一個狀態(tài)相對應，鍵盤輸入或用鼠標選擇一個圖標是使系統(tǒng)進入其他狀盤輸入或用鼠標選擇一個圖標是使系統(tǒng)進

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

20、?，F(xiàn)在的轉(zhuǎn)換規(guī)則形式如下：的函數(shù)。現(xiàn)在的轉(zhuǎn)換規(guī)則形式如下：當前狀態(tài)當前狀態(tài)菜單菜單+事件事件所選擇的項所選擇的項+謂詞謂詞下下個狀態(tài)。個狀態(tài)。為了具體說明怎樣用有窮狀態(tài)機技術(shù)表達系統(tǒng)的規(guī)為了具體說明怎樣用有窮狀態(tài)機技術(shù)表達系統(tǒng)的規(guī)格說明，現(xiàn)在用這種技術(shù)給出大家熟悉的電梯系統(tǒng)格說明，現(xiàn)在用這種技術(shù)給出大家熟悉的電梯系統(tǒng)的規(guī)格說明。首先給出用自然語言描述的對電梯系的規(guī)格說明。首先給出用自然語言描述的對電梯系統(tǒng)的需求：統(tǒng)的需求：在一幢在一幢m層的大廈中需要一套控制層的大廈中需要一套控制n部電梯的產(chǎn)品，部電梯的產(chǎn)品，要求這要求這n部電梯按照約束條件部電梯按照約束條件C1，C2和和C3在樓層在樓層間移動

21、。間移動。C1：每部電梯內(nèi)有：每部電梯內(nèi)有m個按鈕，每個按鈕代表一個樓個按鈕，每個按鈕代表一個樓層。當按下一個按鈕時該按鈕指示燈亮，同時電梯層。當按下一個按鈕時該按鈕指示燈亮，同時電梯駛向相應的樓層，到達按鈕指定的樓層時指示燈熄駛向相應的樓層，到達按鈕指定的樓層時指示燈熄滅。滅。4.2.2 例子例子C2：除了大廈的最低層和最高層之外，每層樓都：除了大廈的最低層和最高層之外，每層樓都有兩個按鈕分別請求電梯上行和下行。這兩個按鈕有兩個按鈕分別請求電梯上行和下行。這兩個按鈕之一被按下時相應的指示燈亮，當電梯到達此樓層之一被按下時相應的指示燈亮，當電梯到達此樓層時燈熄滅，電梯向要求的方向移動。時燈熄滅

22、，電梯向要求的方向移動。C3：當對電梯沒有請求時，它關(guān)門并停在當前樓：當對電梯沒有請求時，它關(guān)門并停在當前樓層。層?，F(xiàn)在使用一個擴展的有窮狀態(tài)機對本產(chǎn)品進行規(guī)格現(xiàn)在使用一個擴展的有窮狀態(tài)機對本產(chǎn)品進行規(guī)格說明。這個問題中有兩個按鈕集。說明。這個問題中有兩個按鈕集。n部電梯中的每部電梯中的每一部都有一部都有m個按鈕，一個按鈕對應一個樓層。因為個按鈕，一個按鈕對應一個樓層。因為這這mn個按鈕都在電梯中，所以稱它們?yōu)殡娞莅磦€按鈕都在電梯中，所以稱它們?yōu)殡娞莅粹o。此外，每層樓有兩個按鈕，一個請求向上，另鈕。此外，每層樓有兩個按鈕，一個請求向上，另一個請求向下，這些按鈕稱為樓層按鈕。一個請求向下，這些按

23、鈕稱為樓層按鈕。電梯按鈕的狀態(tài)轉(zhuǎn)換圖如圖電梯按鈕的狀態(tài)轉(zhuǎn)換圖如圖4.2所示。令所示。令EB(e,f)表表示按下電梯示按下電梯e內(nèi)的按鈕并請求到內(nèi)的按鈕并請求到f層去。層去。EB(e,f)有兩有兩個狀態(tài)，分別是按鈕發(fā)光個狀態(tài)，分別是按鈕發(fā)光(打開打開)和不發(fā)光和不發(fā)光(關(guān)閉關(guān)閉)。更精確地說，狀態(tài)是：更精確地說，狀態(tài)是：EBON(e,f)：電梯按鈕：電梯按鈕(e,f)打開打開EBOFF(e,f)：電梯按鈕：電梯按鈕(e,f)關(guān)閉關(guān)閉如果電梯按鈕如果電梯按鈕(e,f)發(fā)光且電梯到達發(fā)光且電梯到達f層，該按鈕將熄層，該按鈕將熄滅。相反如果按鈕熄滅，則按下它時，按鈕將發(fā)光。滅。相反如果按鈕熄滅，則按下

24、它時，按鈕將發(fā)光。上述描述中包含了兩個事件，它們分別是：上述描述中包含了兩個事件，它們分別是：EBP(e,f)：電梯按鈕：電梯按鈕(e,f)被按下被按下EAF(e,f)：電梯：電梯e到達到達f層層圖圖4.2 電梯按鈕的狀態(tài)轉(zhuǎn)換圖電梯按鈕的狀態(tài)轉(zhuǎn)換圖圖圖4.3樓層按鈕的狀態(tài)轉(zhuǎn)換圖樓層按鈕的狀態(tài)轉(zhuǎn)換圖為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，需要一個謂詞需要一個謂詞V(e,f)，它的含義如下：，它的含義如下：V(e,f)：電梯：電梯e停在停在f層層如果電梯按鈕如果電梯按鈕(e,f)處于關(guān)閉狀態(tài)處于關(guān)閉狀態(tài)當前狀態(tài)當前狀態(tài)，而，而且電梯按鈕且電梯按鈕

25、(e,f)被按下被按下事件事件，而且電梯，而且電梯e不在不在f層層謂詞謂詞，則該電梯按鈕打開發(fā)光，則該電梯按鈕打開發(fā)光下個狀態(tài)下個狀態(tài)。狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下：狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下：EBOFF(e,f)+EBP(e,f)+not V(e,f)EBON(e,f)反之，如果電梯到達反之，如果電梯到達f層，而且電梯按鈕是打開的，層，而且電梯按鈕是打開的，于是它就會熄滅。這條轉(zhuǎn)換規(guī)則可以形式化地表示于是它就會熄滅。這條轉(zhuǎn)換規(guī)則可以形式化地表示為：為：EBON(e,f)+EAF(e,f)EBOFF(e,f)接下來考慮樓層按鈕。令接下來考慮樓層按鈕。令FB(d,f)表示表示f層請求電梯層請求

26、電梯向向d方向運動的按鈕，樓層按鈕方向運動的按鈕，樓層按鈕FB(d,f)的狀態(tài)轉(zhuǎn)換的狀態(tài)轉(zhuǎn)換圖如圖圖如圖4.3所示。所示。樓層按鈕的狀態(tài)如下：樓層按鈕的狀態(tài)如下：FBON(d,f)：樓層按鈕：樓層按鈕(d,f)打開打開FBOFF(d,f)：樓層按鈕：樓層按鈕(d,f)關(guān)閉關(guān)閉如果樓層按鈕已經(jīng)打開，而且一部電梯到達如果樓層按鈕已經(jīng)打開，而且一部電梯到達f層，層，則按鈕關(guān)閉。反之，如果樓層按鈕原來是關(guān)閉的，則按鈕關(guān)閉。反之，如果樓層按鈕原來是關(guān)閉的，被按下后該按鈕將打開。這段敘述中包含了以下兩被按下后該按鈕將打開。這段敘述中包含了以下兩個事件。個事件。FBP(d,f)：樓層按鈕：樓層按鈕(d,f)

27、被按下被按下EAF(1n,f)：電梯：電梯1或或或或n到達到達f層層其中其中1n表示或為表示或為1或為或為2或為或為n。為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，同樣也需要一個謂詞，它是同樣也需要一個謂詞，它是S(d,e,f)，它的定義如下。，它的定義如下。S(d,e,f)：電梯：電梯e停在停在f層并且移動方向由層并且移動方向由d確定為向確定為向上上(d=U)或向下或向下(d=D)或待定或待定(d=N)。這個謂詞實際上是一個狀態(tài)，形式化方法允許把事這個謂詞實際上是一個狀態(tài)，形式化方法允許把事件和狀態(tài)作為謂詞對待。件和狀態(tài)作為謂詞對待。使用謂詞使

28、用謂詞S(d,e,f)，形式化轉(zhuǎn)換規(guī)則為：，形式化轉(zhuǎn)換規(guī)則為：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。也就是說，如果在也就是說，如果在f層請求電梯向?qū)诱埱箅娞菹騞方向運動的樓層方向運動的樓層按鈕處于關(guān)閉狀態(tài)，現(xiàn)在該按鈕被按下，并且當時按鈕處于關(guān)閉狀態(tài)，現(xiàn)在該按鈕被按下，并且當時沒有正停在沒有正停在f層準備向?qū)訙蕚湎騞方向移動的電梯，則該樓層方向移動的電梯，則該樓層按鈕打開。反之，如果樓層按鈕已經(jīng)打開，且至少按鈕打開。反之，如果樓層按鈕已經(jīng)打開，且至

29、少有一部電梯到達有一部電梯到達f層，該部電梯將朝層，該部電梯將朝d方向運動，則方向運動，則按鈕將關(guān)閉。按鈕將關(guān)閉。在討論電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時定義的謂詞在討論電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時定義的謂詞V(e,f)，可以用謂詞可以用謂詞S(d,e,f)重新定義如下：重新定義如下：V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f)定義電梯按鈕和樓層按鈕的狀態(tài)都是很簡單、直觀定義電梯按鈕和樓層按鈕的狀態(tài)都是很簡單、直觀的事情?，F(xiàn)在轉(zhuǎn)向討論電梯的狀態(tài)及其轉(zhuǎn)換規(guī)則，的事情?，F(xiàn)在轉(zhuǎn)向討論電梯的狀態(tài)及其轉(zhuǎn)換規(guī)則，就會出現(xiàn)一些復雜的情況。一個電梯狀態(tài)實質(zhì)上包就會出現(xiàn)一些復雜的情況。一個電梯狀態(tài)實

30、質(zhì)上包含許多子狀態(tài)。含許多子狀態(tài)。下面定義電梯的下面定義電梯的3個狀態(tài)：個狀態(tài)：M(d,e,f)：電梯：電梯e正沿正沿d方向移動，即將到達的是第方向移動，即將到達的是第f層層S(d,e,f)：電梯：電梯e停在停在f層，將朝層，將朝d方向移動方向移動(尚未關(guān)門尚未關(guān)門)W(e,f)：電梯：電梯e在在f層等待層等待(已關(guān)門已關(guān)門)其中其中S(d,e,f)狀態(tài)已在討論樓層按鈕時定義過，但是，狀態(tài)已在討論樓層按鈕時定義過，但是，現(xiàn)在的定義更完備一些?，F(xiàn)在的定義更完備一些。圖圖4.4是電梯的狀態(tài)轉(zhuǎn)換圖。是電梯的狀態(tài)轉(zhuǎn)換圖。3個電梯停止狀態(tài)個電梯停止狀態(tài)S(U,e,f)、S(N,e,f)和和S(D,e,f

31、)已被組合成一個大的狀已被組合成一個大的狀態(tài)，這樣做的目的是減少狀態(tài)總數(shù)以簡化流圖。態(tài)，這樣做的目的是減少狀態(tài)總數(shù)以簡化流圖。圖圖4.4中包含了下述中包含了下述3個可觸發(fā)狀態(tài)發(fā)生改變的事件。個可觸發(fā)狀態(tài)發(fā)生改變的事件。DC(e,f)：電梯：電梯e在樓層在樓層f關(guān)上門關(guān)上門ST(e,f)：電梯：電梯e靠近靠近f層時觸發(fā)傳感器，電梯控制器層時觸發(fā)傳感器，電梯控制器決定在當前樓層電梯是否停下決定在當前樓層電梯是否停下RL：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)，：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)，登錄需求登錄需求圖圖4.4 電梯的狀態(tài)轉(zhuǎn)換圖電梯的狀態(tài)轉(zhuǎn)換圖最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則。為簡單起見，

32、這最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則。為簡單起見，這里給出的規(guī)則僅發(fā)生在關(guān)門之時。里給出的規(guī)則僅發(fā)生在關(guān)門之時。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)第一條規(guī)則表明，如果電梯第一條規(guī)則表明，如果電梯e停在停在f層準備向上移動，層準備向上移動，且門已經(jīng)關(guān)閉，則電梯將向上一樓層移動。第二條且門已經(jīng)關(guān)閉，則電梯將向上一樓層移動。第二條和第三條規(guī)則，分別對應于電梯即將下降或者沒有和第三條規(guī)則，分別對應于電梯即將下降或者沒有待處理的請求的情況。待處理的請求的情況。有窮狀態(tài)機方法采用了一種簡單的格式來描

33、述規(guī)格有窮狀態(tài)機方法采用了一種簡單的格式來描述規(guī)格說明：說明：當前狀態(tài)當前狀態(tài)+事件事件+謂詞謂詞下個狀態(tài)下個狀態(tài)這種形式的規(guī)格說明易于書寫、易于驗證，而且可這種形式的規(guī)格說明易于書寫、易于驗證，而且可以比較容易地把它轉(zhuǎn)變成設(shè)計或程序代碼。事實上，以比較容易地把它轉(zhuǎn)變成設(shè)計或程序代碼。事實上，可以開發(fā)一個可以開發(fā)一個CASE工具把一個有窮狀態(tài)機規(guī)格說工具把一個有窮狀態(tài)機規(guī)格說明直接轉(zhuǎn)變?yōu)樵创a。維護可以通過重新轉(zhuǎn)變來實明直接轉(zhuǎn)變?yōu)樵创a。維護可以通過重新轉(zhuǎn)變來實現(xiàn)，也就是說，如果需要一個新的狀態(tài)或事件，首現(xiàn)，也就是說，如果需要一個新的狀態(tài)或事件，首先修改規(guī)格說明，然后直接由新的規(guī)格說明生成新先

34、修改規(guī)格說明，然后直接由新的規(guī)格說明生成新版本的產(chǎn)品。版本的產(chǎn)品。4.2.3 評價評價有窮狀態(tài)機方法比數(shù)據(jù)流圖技術(shù)更精確，而且和它有窮狀態(tài)機方法比數(shù)據(jù)流圖技術(shù)更精確，而且和它一樣易于理解。不過，它也有缺點：在開發(fā)一個大一樣易于理解。不過，它也有缺點：在開發(fā)一個大系統(tǒng)時三元組系統(tǒng)時三元組(即狀態(tài)、事件、謂詞即狀態(tài)、事件、謂詞)的數(shù)量會迅速的數(shù)量會迅速增長。此外，和數(shù)據(jù)流圖方法一樣，形式化的有窮增長。此外，和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機方法也沒有處理定時需求。下節(jié)將介紹的狀態(tài)機方法也沒有處理定時需求。下節(jié)將介紹的Petri網(wǎng)技術(shù)，是一種可處理定時問題的形式化方法。網(wǎng)技術(shù)，是一種可處理定時問

35、題的形式化方法。并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題。這個并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題。這個問題可以表現(xiàn)為多種形式，如同步問題、競爭條件問題可以表現(xiàn)為多種形式，如同步問題、競爭條件以及死鎖問題。定時問題通常是由不好的設(shè)計或有以及死鎖問題。定時問題通常是由不好的設(shè)計或有錯誤的實現(xiàn)引起的，而這樣的設(shè)計或?qū)崿F(xiàn)通常又是錯誤的實現(xiàn)引起的，而這樣的設(shè)計或?qū)崿F(xiàn)通常又是由不好的規(guī)格說明造成的。如果規(guī)格說明不恰當，由不好的規(guī)格說明造成的。如果規(guī)格說明不恰當，則有導致不完善的設(shè)計或?qū)崿F(xiàn)的危險。用于確定系則有導致不完善的設(shè)計或?qū)崿F(xiàn)的危險。用于確定系統(tǒng)中隱含的定時問題的一種有效技術(shù)是統(tǒng)中隱含的定時問題的一

36、種有效技術(shù)是Petri網(wǎng)，這網(wǎng)，這種技術(shù)的一個很大的優(yōu)點是它也可以用于設(shè)計中。種技術(shù)的一個很大的優(yōu)點是它也可以用于設(shè)計中。4.3 Petri網(wǎng)網(wǎng) 4.3.1 概念概念etri網(wǎng)是由網(wǎng)是由Carl Adam Petri發(fā)明的。最初只有自動發(fā)明的。最初只有自動化專家對化專家對Petri網(wǎng)感興趣，后來網(wǎng)感興趣，后來Petri網(wǎng)在計算機科網(wǎng)在計算機科學中也得到廣泛的應用，例如，在性能評價、操作學中也得到廣泛的應用，例如，在性能評價、操作系統(tǒng)和軟件工程等領(lǐng)域，系統(tǒng)和軟件工程等領(lǐng)域，Petri網(wǎng)應用得都比較廣泛。網(wǎng)應用得都比較廣泛。特別是已經(jīng)證明，用特別是已經(jīng)證明，用Petri網(wǎng)可以有效地描述并發(fā)活網(wǎng)可以

37、有效地描述并發(fā)活動。動。Petri網(wǎng)包含網(wǎng)包含4種元素：一組位置種元素：一組位置P、一組轉(zhuǎn)換、一組轉(zhuǎn)換T、輸、輸入函數(shù)入函數(shù)I以及輸出函數(shù)以及輸出函數(shù)O。圖。圖4.5舉例說明了舉例說明了Petri網(wǎng)網(wǎng)的組成。的組成。圖圖4.5 Petri網(wǎng)的組成網(wǎng)的組成一組位置一組位置P為為P1，P2，P3，P4，在圖中用圓圈，在圖中用圓圈代表位置。代表位置。一組轉(zhuǎn)換一組轉(zhuǎn)換T為為t1，t2，在圖中用短直線表示轉(zhuǎn)，在圖中用短直線表示轉(zhuǎn)換。換。兩個用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭兩個用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭表示，它們是：頭表示，它們是：I(t1)=P2，P4I(t2)=P2兩個用于轉(zhuǎn)換

38、的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭兩個用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭表示，它們是：頭表示，它們是：O(t1)=P1O(t2)=P3，P3注意，輸出函數(shù)注意，輸出函數(shù)O(t2)中有兩個中有兩個P3，是因為有兩個，是因為有兩個箭頭由箭頭由t2指向指向P3。更形式化的更形式化的Petri網(wǎng)結(jié)構(gòu)，是一個四元組網(wǎng)結(jié)構(gòu)，是一個四元組C=(P,T,I,O)。其中，其中，P=P1，Pn是一個有窮位置集，是一個有窮位置集，n0。T=t1，tm是一個有窮轉(zhuǎn)換集，是一個有窮轉(zhuǎn)換集，m0，且，且T和和P不相交。不相交。I：TP為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組(bags

39、)的映射。的映射。O：TP為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射。組的映射。一個無序單位組或多重組是允許一個元素有多個實一個無序單位組或多重組是允許一個元素有多個實例的廣義集。例的廣義集。Petri網(wǎng)的標記是在網(wǎng)的標記是在Petri網(wǎng)中權(quán)標網(wǎng)中權(quán)標(token)的分配。的分配。例如，在圖例如，在圖4.6中有中有4個權(quán)標，其中一個在個權(quán)標，其中一個在P1中，兩中，兩個在個在P2中，中，P3中沒有，還有一個在中沒有，還有一個在P4中。上述標中。上述標記可以用向量記可以用向量(1，2，0，1)表示。由于表示。由于P2和和P4中有中有權(quán)標，因此權(quán)標，因此t1啟動啟

40、動(即被激發(fā)即被激發(fā))。通常，當每個輸入。通常，當每個輸入位置所擁有的權(quán)標數(shù)大于等于從該位置到轉(zhuǎn)換的線位置所擁有的權(quán)標數(shù)大于等于從該位置到轉(zhuǎn)換的線數(shù)時，就允許轉(zhuǎn)換。當數(shù)時，就允許轉(zhuǎn)換。當t1被激發(fā)時，被激發(fā)時，P2和和P4上各有上各有一個權(quán)標被移出，而一個權(quán)標被移出，而P1上則增加一個權(quán)標。上則增加一個權(quán)標。Petri網(wǎng)中權(quán)標總數(shù)不是固定的，在這個例子中兩個權(quán)標網(wǎng)中權(quán)標總數(shù)不是固定的，在這個例子中兩個權(quán)標被移出，而被移出，而P1上只能增加一個權(quán)標。上只能增加一個權(quán)標。在圖在圖4.6中中P2上有權(quán)標，因此上有權(quán)標，因此t2也可以被激發(fā)。當也可以被激發(fā)。當t2被激發(fā)時，被激發(fā)時，P2上將移走一個權(quán)

41、標，而上將移走一個權(quán)標，而P3上新增加上新增加兩個權(quán)標。兩個權(quán)標。Petri網(wǎng)具有非確定性，也就是說，如果網(wǎng)具有非確定性，也就是說，如果數(shù)個轉(zhuǎn)換都達到了激發(fā)條件，則其中任意一個都可數(shù)個轉(zhuǎn)換都達到了激發(fā)條件，則其中任意一個都可以被激發(fā)。圖以被激發(fā)。圖4.6所示所示Petri網(wǎng)的標記為網(wǎng)的標記為(1，2，0，1)，t1和和t2都可以被激發(fā)。假設(shè)都可以被激發(fā)。假設(shè)t1被激發(fā)了，則結(jié)果如被激發(fā)了，則結(jié)果如圖圖4.7所示，標記為所示，標記為(2，1，0，0)。此時，只有。此時，只有t2可可以被激發(fā)。如果以被激發(fā)。如果t2也被激發(fā)了，則權(quán)標從也被激發(fā)了，則權(quán)標從P2中移出，中移出，兩個新權(quán)標被放在兩個新權(quán)

42、標被放在P3上，結(jié)果如圖上，結(jié)果如圖4.8所示，標記所示，標記為為(2，0，2，0)。圖圖4.6 帶標記的帶標記的Petri網(wǎng)網(wǎng)圖圖4.7 圖圖4.6的的Petri網(wǎng)在轉(zhuǎn)換網(wǎng)在轉(zhuǎn)換 t1被激發(fā)后的情況被激發(fā)后的情況圖圖4.8 圖圖4.7的的Petri網(wǎng)在轉(zhuǎn)換網(wǎng)在轉(zhuǎn)換 t2被激發(fā)后的情況被激發(fā)后的情況圖圖4.9 含禁止線的含禁止線的Petri網(wǎng)網(wǎng)更形式化地說，更形式化地說，Petri網(wǎng)網(wǎng)C=(P，T，I，O)中的標記中的標記M，是由一組位置，是由一組位置P到一組非負整數(shù)的映射：到一組非負整數(shù)的映射：M：P0，1，2，這樣，帶有標記的這樣，帶有標記的Petri網(wǎng)成為一個五元組網(wǎng)成為一個五元組(P，

43、T，I，O，M)。對對Petri網(wǎng)的一個重要擴充是加入禁止線。如圖網(wǎng)的一個重要擴充是加入禁止線。如圖4.9所示，禁止線是用一個小圓圈而不是用箭頭標記的所示，禁止線是用一個小圓圈而不是用箭頭標記的輸入線。通常，當每個輸入線上至少有一個權(quán)標，輸入線。通常，當每個輸入線上至少有一個權(quán)標，而禁止線上沒有權(quán)標的時候，相應的轉(zhuǎn)換才是允許而禁止線上沒有權(quán)標的時候，相應的轉(zhuǎn)換才是允許的。在圖的。在圖4.9中，中，P3上有一個權(quán)標而上有一個權(quán)標而P2上沒有權(quán)標，上沒有權(quán)標，因此轉(zhuǎn)換因此轉(zhuǎn)換t1可以被激發(fā)?？梢员患ぐl(fā)。現(xiàn)在把現(xiàn)在把Petri網(wǎng)應用于上一節(jié)討論過的電梯問題。當網(wǎng)應用于上一節(jié)討論過的電梯問題。當用用P

44、etri網(wǎng)表示電梯系統(tǒng)的規(guī)格說明時，每個樓層用網(wǎng)表示電梯系統(tǒng)的規(guī)格說明時，每個樓層用一個位置一個位置Ff代表代表(1fm)，在，在Petri網(wǎng)中電梯是用一網(wǎng)中電梯是用一個權(quán)標代表的。在位置個權(quán)標代表的。在位置Ff上有權(quán)標，表示在樓層上有權(quán)標，表示在樓層f上有電梯。上有電梯。1. 電梯按鈕電梯按鈕電梯問題的第一個約束條件描述了電梯按鈕的行為，電梯問題的第一個約束條件描述了電梯按鈕的行為，現(xiàn)在復述一下這個約束條件。現(xiàn)在復述一下這個約束條件。4.3.2 例子例子第一條約束第一條約束C1：每部電梯有：每部電梯有m個按鈕，每層對應一個按鈕，每層對應一個按鈕。當按下一個按鈕時該按鈕指示燈亮，指示個按鈕。當

45、按下一個按鈕時該按鈕指示燈亮，指示電梯移往相應的樓層。當電梯到達指定的樓層時，電梯移往相應的樓層。當電梯到達指定的樓層時，按鈕將熄滅。按鈕將熄滅。為了用為了用Petri網(wǎng)表達電梯按鈕的規(guī)格說明，在網(wǎng)表達電梯按鈕的規(guī)格說明，在Petri網(wǎng)中還必須設(shè)置其他的位置。電梯中樓層網(wǎng)中還必須設(shè)置其他的位置。電梯中樓層f的按鈕，的按鈕，在在Petri網(wǎng)中用位置網(wǎng)中用位置EBf表示表示(1fm)。在。在EBf上有一上有一個權(quán)標，就表示電梯內(nèi)樓層個權(quán)標，就表示電梯內(nèi)樓層f的按鈕被按下了。的按鈕被按下了。電梯按鈕只有在第一次被按下時才會由暗變亮，以電梯按鈕只有在第一次被按下時才會由暗變亮，以后再按它則只會被忽略。

46、圖后再按它則只會被忽略。圖4.10所示的所示的Petri網(wǎng)準確網(wǎng)準確地描述了電梯按鈕的行為規(guī)律。首先，假設(shè)按鈕沒地描述了電梯按鈕的行為規(guī)律。首先，假設(shè)按鈕沒有發(fā)亮，顯然在位置有發(fā)亮，顯然在位置EBf上沒有權(quán)標，從而在存在上沒有權(quán)標，從而在存在禁止線的情況下，轉(zhuǎn)換禁止線的情況下，轉(zhuǎn)換“EBf被按下被按下”是允許發(fā)生是允許發(fā)生的。假設(shè)現(xiàn)在按下按鈕，則轉(zhuǎn)換被激發(fā)并在的。假設(shè)現(xiàn)在按下按鈕，則轉(zhuǎn)換被激發(fā)并在EBf上上放置了一個權(quán)標，如圖放置了一個權(quán)標，如圖4.10所示。以后不論再按下所示。以后不論再按下多少次按鈕，禁止線與現(xiàn)有權(quán)標的組合都決定了轉(zhuǎn)多少次按鈕，禁止線與現(xiàn)有權(quán)標的組合都決定了轉(zhuǎn)換換“EBf被

47、按下被按下”不能再被激發(fā)了，因此，位置不能再被激發(fā)了，因此，位置EBf上的權(quán)標數(shù)不會多于上的權(quán)標數(shù)不會多于1。圖圖4.10 Petri網(wǎng)表示的電梯按鈕網(wǎng)表示的電梯按鈕假設(shè)電梯由假設(shè)電梯由g層駛向?qū)玉傁騠層，因為電梯在層，因為電梯在g層，如圖層，如圖4.10所示，位置所示，位置Fg上有一個權(quán)標。由于每條輸入線上各上有一個權(quán)標。由于每條輸入線上各有一個權(quán)標，轉(zhuǎn)換有一個權(quán)標，轉(zhuǎn)換“電梯在運行電梯在運行”被激發(fā)，從而被激發(fā)，從而EBf和和Fg上的權(quán)標被移走，按鈕上的權(quán)標被移走，按鈕EBf被關(guān)閉，在位被關(guān)閉，在位置置Ff上出現(xiàn)一個新權(quán)標，即轉(zhuǎn)換的激發(fā)使電梯由上出現(xiàn)一個新權(quán)標，即轉(zhuǎn)換的激發(fā)使電梯由g層駛到

48、層駛到f層。層。事實上，電梯由事實上，電梯由g層移到層移到f層是需要時間的，為處理層是需要時間的，為處理這個情況及其他類似的問題這個情況及其他類似的問題(例如，由于物理上的例如，由于物理上的原因按鈕被按下后不能馬上發(fā)亮原因按鈕被按下后不能馬上發(fā)亮)，Petri網(wǎng)模型中網(wǎng)模型中必須加入時限。也就是說，在標準必須加入時限。也就是說，在標準Petri網(wǎng)中轉(zhuǎn)換是網(wǎng)中轉(zhuǎn)換是瞬時完成的，而在現(xiàn)實情況下就需要時間控制瞬時完成的，而在現(xiàn)實情況下就需要時間控制Petri網(wǎng)，以使轉(zhuǎn)換與非零時間相聯(lián)系。網(wǎng)，以使轉(zhuǎn)換與非零時間相聯(lián)系。2. 樓層按鈕樓層按鈕在第二個約束條件中描述了樓層按鈕的行為。在第二個約束條件中描述

49、了樓層按鈕的行為。第二條約束第二條約束C2：除了第一層與頂層之外，每個樓：除了第一層與頂層之外，每個樓層都有兩個按鈕，一個要求電梯上行，另一個要求層都有兩個按鈕，一個要求電梯上行，另一個要求電梯下行。這些按鈕在按下時發(fā)亮，當電梯到達該電梯下行。這些按鈕在按下時發(fā)亮，當電梯到達該層并將向指定方向移動時，相應的按鈕才會熄滅。層并將向指定方向移動時，相應的按鈕才會熄滅。在在Petri網(wǎng)中樓層按鈕用位置網(wǎng)中樓層按鈕用位置FBfu和和FBfd表示，分別表示，分別代表代表f樓層請求電梯上行和下行的按鈕。底層的按樓層請求電梯上行和下行的按鈕。底層的按鈕為鈕為FB1u，最高層的按鈕為，最高層的按鈕為FBmd，

50、中間每一層有，中間每一層有兩個按鈕兩個按鈕FBfu和和FBfd(1fm)。圖圖4.11 Petri網(wǎng)表示樓層按鈕網(wǎng)表示樓層按鈕圖圖4.11所示的情況為電梯由所示的情況為電梯由g層駛向?qū)玉傁騠層。根據(jù)電梯層。根據(jù)電梯乘客的要求，某一個樓層按鈕亮或兩個樓層按鈕都乘客的要求，某一個樓層按鈕亮或兩個樓層按鈕都亮。如果兩個按鈕都亮了，則只有一個按鈕熄滅。亮。如果兩個按鈕都亮了，則只有一個按鈕熄滅。圖圖4.11所示的所示的Petri網(wǎng)可以保證，當兩個按鈕都亮了網(wǎng)可以保證，當兩個按鈕都亮了的時候，只有一個按鈕熄滅。但是要保證按鈕熄滅的時候，只有一個按鈕熄滅。但是要保證按鈕熄滅正確，則需要更復雜的正確，則需要

51、更復雜的Petri網(wǎng)模型。網(wǎng)模型。最后，考慮第三條約束。最后，考慮第三條約束。第三條約束第三條約束C3：當電梯沒有收到請求時，它將停：當電梯沒有收到請求時，它將停留在當前樓層并關(guān)門。留在當前樓層并關(guān)門。這條約束很容易實現(xiàn)，如圖這條約束很容易實現(xiàn)，如圖4.11所示，當沒有請求所示，當沒有請求(FBfu和和FBfd上無權(quán)標）時，任何一個轉(zhuǎn)換上無權(quán)標）時，任何一個轉(zhuǎn)換“電梯電梯在運行在運行”都不能被激發(fā)。都不能被激發(fā)。用用Z語言描述的、最簡單的形式化規(guī)格說明含有下語言描述的、最簡單的形式化規(guī)格說明含有下述述4個部分：個部分：給定的集合、數(shù)據(jù)類型及常數(shù)。給定的集合、數(shù)據(jù)類型及常數(shù)。狀態(tài)定義。狀態(tài)定義。

52、初始狀態(tài)。初始狀態(tài)。操作。操作。4.4 Z語言語言 4.4.1 簡介簡介1. 給定的集合給定的集合一個一個Z規(guī)格說明從一系列給定的初始化集合開始。規(guī)格說明從一系列給定的初始化集合開始。所謂初始化集合就是不需要詳細定義的集合，這種所謂初始化集合就是不需要詳細定義的集合，這種集合用帶方括號的形式表示。對于電梯問題，給定集合用帶方括號的形式表示。對于電梯問題，給定的初始化集合稱為的初始化集合稱為Button，即所有按鈕的集合，因，即所有按鈕的集合，因此，此，Z規(guī)格說明開始于：規(guī)格說明開始于：Button2. 狀態(tài)定義狀態(tài)定義一個一個Z規(guī)格說明由若干個規(guī)格說明由若干個“格格(schema)”組成，每個

53、組成，每個格含有一組變量說明和一系列限定變量取值范圍的格含有一組變量說明和一系列限定變量取值范圍的謂詞。例如，格謂詞。例如，格S的格式如圖的格式如圖4.12所示。所示。圖圖4.12 Z格格S的格式的格式在電梯問題中，在電梯問題中，Button有有4個子集，即個子集，即floor_buttons(樓層按鈕的集合樓層按鈕的集合)、elevator_buttons(電梯按鈕的集合電梯按鈕的集合)、buttons(電梯電梯問題中所有按鈕的集合問題中所有按鈕的集合)以及以及pushed(所有被按的按所有被按的按鈕的集合，即所有處于打開狀態(tài)的按鈕的集合鈕的集合，即所有處于打開狀態(tài)的按鈕的集合)。圖圖4.1

54、3（見書（見書76頁）描述了格頁）描述了格Button_State，其中，其中，符號符號P表示冪集表示冪集(即給定集的所有子集即給定集的所有子集)。約束條件。約束條件聲明，聲明，floor_buttons集與集與elevator_buttons集不相交，集不相交，而且它們共同組成而且它們共同組成buttons集集(在下面的討論中并不在下面的討論中并不需要需要floor_buttons集和集和elevator_buttons集，把它們集，把它們放于圖放于圖4.13中只是用來說明中只是用來說明Z格包含的內(nèi)容格包含的內(nèi)容)。3. 初始狀態(tài)初始狀態(tài)抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。對抽象的初始

55、狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。對于電梯問題來說，抽象的初始狀態(tài)為：于電梯問題來說，抽象的初始狀態(tài)為：Button_InitButton_Statepushed=上式表示，當系統(tǒng)首次開啟時上式表示，當系統(tǒng)首次開啟時pushed集為空，即所集為空，即所有按鈕都處于關(guān)閉狀態(tài)。有按鈕都處于關(guān)閉狀態(tài)。4. 操作操作如果一個原來處于關(guān)閉狀態(tài)的按鈕被按下，則該按如果一個原來處于關(guān)閉狀態(tài)的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到鈕開啟，這個按鈕就被添加到pushed集中。圖集中。圖4.14（見書（見書77頁）定義了操作頁）定義了操作Push_Button(按按鈕按按鈕)。 操作的謂詞部分，包含了一組調(diào)用

56、操作的前置條件，操作的謂詞部分，包含了一組調(diào)用操作的前置條件，以及操作完全結(jié)束后的后置條件。如果前置條件成以及操作完全結(jié)束后的后置條件。如果前置條件成立，則操作執(zhí)行完成后可得到后置條件。但是，如立，則操作執(zhí)行完成后可得到后置條件。但是，如果在前置條件不成立的情況下調(diào)用該操作，則不能果在前置條件不成立的情況下調(diào)用該操作，則不能得到指定的結(jié)果得到指定的結(jié)果(因此結(jié)果無法預測因此結(jié)果無法預測)。假設(shè)電梯到達了某樓層，如果相應的樓層按鈕已經(jīng)假設(shè)電梯到達了某樓層，如果相應的樓層按鈕已經(jīng)打開，則此時它會關(guān)閉；同樣，如果相應的電梯按打開，則此時它會關(guān)閉；同樣，如果相應的電梯按鈕已經(jīng)打開，則此時它也會關(guān)閉。也

57、就是說，如果鈕已經(jīng)打開，則此時它也會關(guān)閉。也就是說，如果“button?”屬于屬于pushed集，則將它移出該集合，如集，則將它移出該集合，如圖圖4.15（見書（見書77頁）所示頁）所示(符號符號“”表示集合差運表示集合差運算算)。已經(jīng)在許多軟件開發(fā)項目中成功地運用了已經(jīng)在許多軟件開發(fā)項目中成功地運用了Z語言，語言，目前，目前，Z也許是應用得最廣泛的形式化語言，尤其也許是應用得最廣泛的形式化語言，尤其是在大型項目中是在大型項目中Z語言的優(yōu)勢更加明顯。語言的優(yōu)勢更加明顯。Z語言之語言之所以會獲得如此多的成功，主要有以下幾個原因：所以會獲得如此多的成功，主要有以下幾個原因：(1) 可以比較容易地發(fā)

58、現(xiàn)用可以比較容易地發(fā)現(xiàn)用Z寫的規(guī)格說明的錯誤，寫的規(guī)格說明的錯誤，特別是在自己審查規(guī)格說明，及根據(jù)形式化的規(guī)格特別是在自己審查規(guī)格說明，及根據(jù)形式化的規(guī)格說明來審查設(shè)計與代碼時，情況更是如此。說明來審查設(shè)計與代碼時，情況更是如此。(2) 用用Z寫規(guī)格說明時，要求作者十分精確地使用寫規(guī)格說明時，要求作者十分精確地使用Z說明符。由于對精確性的要求很高，從而和非形式說明符。由于對精確性的要求很高，從而和非形式化規(guī)格說明相比，減少了模糊性、不一致性和遺漏?；?guī)格說明相比，減少了模糊性、不一致性和遺漏。4.4.2 評價評價(3) Z是一種形式化語言，在需要時開發(fā)者可以嚴格是一種形式化語言，在需要時開發(fā)者

59、可以嚴格地驗證規(guī)格說明的正確性。地驗證規(guī)格說明的正確性。(4) 雖然完全學會雖然完全學會Z語言相當困難，但是，經(jīng)驗表明，語言相當困難，但是，經(jīng)驗表明，只學過中學數(shù)學的軟件開發(fā)人員仍然可以只用比較只學過中學數(shù)學的軟件開發(fā)人員仍然可以只用比較短的時間就學會編寫短的時間就學會編寫Z規(guī)格說明，當然，這些人還規(guī)格說明，當然，這些人還沒有能力證明規(guī)格說明的結(jié)果是否正確。沒有能力證明規(guī)格說明的結(jié)果是否正確。(5) 使用使用Z語言可以降低軟件開發(fā)費用。雖然用語言可以降低軟件開發(fā)費用。雖然用Z寫寫規(guī)格說明所需用的時間比使用非形式化技術(shù)要多，規(guī)格說明所需用的時間比使用非形式化技術(shù)要多，但開發(fā)過程所需要的總時間卻減

60、少了。但開發(fā)過程所需要的總時間卻減少了。(6) 雖然用戶無法理解用雖然用戶無法理解用Z寫的規(guī)格說明，但是，可寫的規(guī)格說明，但是，可以依據(jù)以依據(jù)Z規(guī)格說明用自然語言重寫規(guī)格說明。經(jīng)驗規(guī)格說明用自然語言重寫規(guī)格說明。經(jīng)驗證明，這樣得到的自然語言規(guī)格說明，比直接用自證明，這樣得到的自然語言規(guī)格說明，比直接用自然語言寫出的非形式化規(guī)格說明更清楚、更正確。然語言寫出的非形式化規(guī)格說明更清楚、更正確。使用形式化規(guī)格說明是全球的總趨勢，過去，主要使用形式化規(guī)格說明是全球的總趨勢，過去，主要是歐洲習慣于使用形式化規(guī)格說明技術(shù)，現(xiàn)在越來是歐洲習慣于使用形式化規(guī)格說明技術(shù)，現(xiàn)在越來越多的美國公司也開始使用形式化規(guī)