軟件工程導(dǎo)論第4章形式化說明技術(shù)

1、形式化說明技術(shù)按照形式化的程度，可以把軟件工程使用的方法劃分成非形式化，半形式化和形式化3類。用自然語言描述需求規(guī)格說明，是典型的非形式化方法。用數(shù)據(jù)流圖或?qū)嶓w了解圖建 立模型，是典型的半形式化方法。所謂形式化方法，是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)，也就是說，如果一種方法有堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)，那么它就是形式化的。4.1 概述4.1.1 非形式化方法的缺點(diǎn)用自然語言書寫的系統(tǒng)規(guī)格說明書，可能存在矛盾、二義性、含糊性、不完整性及抽象層次混亂等問題。所謂矛盾是指一組相互沖突的陳述。例如，規(guī)格說明書的某一部分可能規(guī)定系統(tǒng)必須監(jiān)控化學(xué)反應(yīng)容器中的溫度，而另一部分（可能由另一位系統(tǒng)分析員撰寫）卻規(guī)定只監(jiān)控在一定

2、范圍內(nèi)的溫度。如果這兩個相互矛盾的規(guī)定寫在同一頁紙上，自然很容易查出，不幸的是，它們往往出現(xiàn)在相距幾十頁甚至數(shù)百頁的兩頁紙中。二義性是指讀者可以用不同方式理解的陳述。例如，下面的陳述就是具有二義性：“操作員標(biāo)識由操作員姓名和密碼組成，密碼由6位數(shù)字構(gòu)成。當(dāng)操作員登錄進(jìn)系統(tǒng)時它被存放在注冊文件中。”在上面這段陳述中，“它”到底代表“密碼”還是“操作員標(biāo)識”，不同的人往往有不同的理解。系統(tǒng)規(guī)格說明書是很龐大的文檔，因此，幾乎不可避免地會出現(xiàn)含糊性。例如，我們可能經(jīng)常在文檔中看到類似下面這樣的需求：“系統(tǒng)界面應(yīng)該是對用戶友好的。”實(shí)際上，這樣籠統(tǒng)的陳述并沒有給出任何有用的信息。不完整性可能是在系統(tǒng)規(guī)

3、格說明中最常遇到的問題之一。例如，考慮下述的系統(tǒng)功能需求：“系統(tǒng)每小時從安放在水庫中的深度傳感器獲取一次水庫深度數(shù)據(jù)，這些數(shù)值應(yīng)該保留6個月?！奔僭O(shè)在系統(tǒng)規(guī)格說明書中還規(guī)定了某個命令的功能：“AVERAGE命令的功能是，在PC機(jī)上顯示由某個傳感器在兩個日期之間獲取的平均水深?！比绻谝?guī)格說明書中對這個命令的功能沒有更多的描述，那么，該命令的細(xì)節(jié)是嚴(yán)重不完整的，例如，對該命令的描述沒有告訴我們，如果用戶給定的日期是在當(dāng)前日期的6個月之前，那么系統(tǒng)應(yīng)該做什么。抽象層次混亂是指在非常抽象的陳述中混進(jìn)了一些關(guān)于細(xì)節(jié)的低層次陳述。這樣的規(guī)格說明書使得讀者很難了解系統(tǒng)的整體功能結(jié)構(gòu)。4.1.2 形式化方法

4、的優(yōu)點(diǎn)正如上一小節(jié)所講的，人在理解用自然語言描述的規(guī)格說明時，容易產(chǎn)生二義性。為了克服非形式化方法的缺點(diǎn)，人們把數(shù)學(xué)引入軟件開發(fā)過程，創(chuàng)造了基于數(shù)學(xué)的形式化方法。在開發(fā)大型軟件系統(tǒng)的過程中應(yīng)用數(shù)學(xué)，能夠帶來下述的幾個優(yōu)點(diǎn)：數(shù)學(xué)最有用的一個性質(zhì)是，它能夠簡潔準(zhǔn)確地描述物理現(xiàn)象、對象或動作的結(jié)果，因此是理想的建模工具。數(shù)學(xué)特別適合于表示狀態(tài)，也就是表示“做什么”。需求規(guī)格說明書主要描述應(yīng)用系統(tǒng)在運(yùn)行前和運(yùn)行后的狀態(tài)，因此，數(shù)學(xué)比自然語言更適于描述詳細(xì)的需求。在理想情況下，分析員可以寫出系統(tǒng)的數(shù)學(xué)規(guī)格說明，它準(zhǔn)確到幾乎沒有二義性，而且可以用數(shù)學(xué)方法來驗(yàn)證，以發(fā)現(xiàn)存在的矛盾和不完整性，在這樣的規(guī)格說明

5、中完全沒有含糊性。但是，實(shí)際情況并不這么簡單，軟件系統(tǒng)的復(fù)雜性是出了名的，希望用少數(shù)幾個數(shù)學(xué)公式來描述它，是根本不可能的。此外，即使應(yīng)用了形式化方法，完整性也是難于保證的：由于溝通不夠，可能遺漏了客戶的一些需求；規(guī)格說明的撰寫者可能有意省略了系統(tǒng)的某些特征，以便設(shè)計(jì)者在選擇實(shí)現(xiàn)方法時有一定自由度；要設(shè)想出使用一個大型復(fù)雜系統(tǒng)的每一個可能的情景，通常是做不到的。在軟件開發(fā)過程中使用數(shù)學(xué)的另一個優(yōu)點(diǎn)是，可以在不同的軟件工程活動之間平滑地過渡。不僅功能規(guī)格說明，而且系統(tǒng)設(shè)計(jì)也可以用數(shù)學(xué)表達(dá)，當(dāng)然，程序代碼也是一種數(shù)學(xué)符號（雖然是一種相當(dāng)繁瑣、冗長的數(shù)學(xué)符號）。數(shù)學(xué)作為軟件開發(fā)工具的最后一個優(yōu)點(diǎn)是，它

6、提供了高層確認(rèn)的手段?？梢允褂脭?shù)學(xué)方法證明，設(shè)計(jì)符合規(guī)格說明，程序代碼正確地實(shí)現(xiàn)了設(shè)計(jì)結(jié)果。4.1.3 應(yīng)用形式化方法的準(zhǔn)則人們對形式方法的看法并不一致。形式化方法對某些軟件工程師很有吸引力，其擁護(hù)者甚至宣稱這種方法可以引發(fā)軟件方法的革命：另一些人則對把數(shù)學(xué)引入軟件開發(fā)過程持懷疑甚至反對的態(tài)度。編者認(rèn)為，對形式化方法也應(yīng)該“一分為二”，既不要過分夸大它的優(yōu)點(diǎn)也不要一概排斥。為了更好地發(fā)揮這種方法的長處，下面給出應(yīng)用形式化方法的幾條準(zhǔn)則，供讀者在實(shí)際工作中使用。（1） 應(yīng)該用適當(dāng)?shù)谋硎痉椒?。通常，一種規(guī)格說明技術(shù)只能用自然的方式說明某一類概念，如果用這種技術(shù)描述其不適于描述的概念，則不僅工作量大

7、而且描述方式也很復(fù)雜。例如，Z語言并不適于說明并發(fā)性。因此，應(yīng)該仔細(xì)選擇一種適用開當(dāng)前項(xiàng)目的形式化說明技術(shù)。（2） 應(yīng)該形式化，但不要過分形式化。目前的形式化技術(shù)還不適于描述系統(tǒng)的每個方面。例如，示例屏幕和自然語言可能還是目前描述用戶界面的可視特性的最佳方法。但是，也不能因此就認(rèn)為完全沒必要采用形式化方法。形式化規(guī)格說明技術(shù)要求我們非常準(zhǔn)確地描述事物，因此有助于防止含糊和誤解。事實(shí)上，如果用形式化方法仔細(xì)說明系統(tǒng)中易出錯的或關(guān)鍵的部分，則只用適中的工作量就能獲得較大回報。（3） 應(yīng)該估算成本。為了使用形式化方法，通常需要事先進(jìn)行大量的培訓(xùn)，最好預(yù)先估算所需的成本并編入預(yù)算。（4） 應(yīng)該有形式化

8、方法顧問隨時提供咨詢。絕大多數(shù)軟件工程師對形式化方法中使用的數(shù)學(xué)和邏輯并不很熟悉，而且沒受過使用形式化方法的專業(yè)訓(xùn)練，因此，需要專家指導(dǎo)和培訓(xùn)。（5） 不應(yīng)該放棄傳統(tǒng)的開發(fā)方法。把形式化方法和結(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋硎强赡艿?，而且由于取長補(bǔ)短往往能獲得很好的效果。（6） 應(yīng)該建立詳細(xì)的文檔。建議使用自然語言注釋形式化的規(guī)格說明書，以幫助用戶和維護(hù)人員理解系統(tǒng)。（7） 不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)。形式化方法并不能保證軟件的正確性，它們只不過是有助于開發(fā)出高質(zhì)量軟件的一種手段。除了使用形式化說明技術(shù)外，在系統(tǒng)開發(fā)過程中仍然必須一如既往地實(shí)施其他質(zhì)量保證活動。（8） 不應(yīng)該盲目依賴形式化方法。這種方

9、法不是包治百病的靈丹妙藥，它們只不過是眾多工具中的一種。形式化方法并不能保證開發(fā)出的軟件絕對是正確，例如，無法用形式化方法證明從非形式化需求到形式化規(guī)格說明的轉(zhuǎn)換是正確的，因此，必須用其它方法（例如，評審，測試）來驗(yàn)證軟件正確性。（9） 應(yīng)該測試，測試再測試。形式化方法不僅不能保證軟件系統(tǒng)絕對正確，也不能證明系統(tǒng)性能或其他質(zhì)量指標(biāo)符合需要，因此，軟件測試的重要性并沒有降低。（10） 應(yīng)該重用。即使采用了形式化方法，軟件重用仍然是降低軟件成本和提高軟件質(zhì)量的惟一合理的方法，而且用形式化方法說明的軟件構(gòu)件具有清晰定義的功能和接口，使得它們有更好的可重用性。4.2有窮狀態(tài)機(jī)利用有窮狀態(tài)機(jī)可以準(zhǔn)確地描

10、述一個系統(tǒng)，因此它是表達(dá)規(guī)格說明的一種形式化方法。4.2.1概念下面通過一個簡單例子介紹有窮狀態(tài)機(jī)的基本概念。一個保險箱上裝了一個復(fù)合鎖，鎖有三個位置，分別標(biāo)記為1、2、3，轉(zhuǎn)盤可向左（L）或向右(R)轉(zhuǎn)動。這樣，在任意時刻轉(zhuǎn)盤都有6種可能的運(yùn)動，即時1L、1R、2L、2R、3L和3R。保險箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤的任何其他運(yùn)動都將引起報警。圖4.1描繪了保險箱的狀態(tài)轉(zhuǎn)換情況。有一個初始態(tài)，即保險箱鎖定狀態(tài)。若輸入為1L，則下一個狀態(tài)為A，但是，若輸入不是 1L而是轉(zhuǎn)盤的任何其他移動，則下一個狀態(tài)為“報警”，報警是兩個終態(tài)之一（另一個終態(tài)是“保險箱解鎖”）。如果選擇了轉(zhuǎn)盤移動的正確

11、組合，則保險箱狀態(tài)轉(zhuǎn)換的序列為從保險箱鎖定到A再到B，最后到保險箱解鎖，即另外一個終態(tài)。圖4.1是一個有窮狀態(tài)機(jī)的狀態(tài)轉(zhuǎn)態(tài)轉(zhuǎn)換圖。狀態(tài)轉(zhuǎn)換并不一定要用圖形方式描述，表4.1 的表格形式也可以表達(dá)同樣的信息。除了兩個終態(tài)之外，保險箱的其他狀態(tài)將根據(jù)轉(zhuǎn)盤的轉(zhuǎn)動方式轉(zhuǎn)換到下一個狀態(tài)。圖4.1 保險箱的狀態(tài)轉(zhuǎn)換圖初始態(tài) 終態(tài) 轉(zhuǎn)盤的任何其它移動轉(zhuǎn)盤的任何其它移動轉(zhuǎn)盤的任何其它移動 報警終態(tài) 保險箱解鎖2L B3R A1L保險箱鎖定表4.1 保險箱的狀態(tài)轉(zhuǎn)換表報警報警報警3R3L 2L1R1LBA保險箱鎖定保險箱解鎖報警報警報警報警報警報警報警B報警報警報警報警2R報警A轉(zhuǎn)盤動作作次態(tài)當(dāng)前狀態(tài) 從上面這

12、個簡單的例子可以看出，一個有窮狀態(tài)機(jī)包括下述5個部分：狀態(tài)集J、輸入集K、由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個狀態(tài)（次態(tài)）的轉(zhuǎn)換函數(shù)T，初始態(tài)S和終態(tài)集F。對于保險箱的例子，相應(yīng)的有窮狀態(tài)機(jī)的各部分如下。狀態(tài)集：。輸入集轉(zhuǎn)換函數(shù)如表4.1所示。初始態(tài)保險箱鎖定。終態(tài)集。如果使用更形式化的術(shù)語，一個有窮狀態(tài)機(jī)可以表示為一個5元組（），其中：；（）；有窮狀態(tài)機(jī)的概念在計(jì)算機(jī)系統(tǒng)中應(yīng)用得非常廣泛。例如，每個菜單驅(qū)動的用戶界面都是一個有窮狀態(tài)機(jī)的實(shí)現(xiàn)。一個菜單的顯示和一個狀態(tài)相對應(yīng)，鍵盤輸入或用鼠標(biāo)選擇一個圖標(biāo)是使系統(tǒng)進(jìn)入其他狀態(tài)的一個事件。狀態(tài)的每個轉(zhuǎn)換都具有下面的形式：當(dāng)前狀態(tài)菜單+事件所選擇的項(xiàng) 下個

13、狀態(tài)。為了對一個系統(tǒng)進(jìn)行規(guī)格說明，通常都需要對有窮狀態(tài)機(jī)做一個很有用的擴(kuò)展，即在前述的5元組中加入6個組件謂詞集P，從而把有窮狀態(tài)機(jī)擴(kuò)展為一個6元組，其中每個謂詞都是系統(tǒng)全局狀態(tài)Y的函數(shù)。轉(zhuǎn)換函數(shù)T現(xiàn)在是一個從（） 到J的函數(shù)?，F(xiàn)在的轉(zhuǎn)換規(guī)則形式如下： 當(dāng)前狀態(tài) 菜單 +事件 所選擇的項(xiàng)+謂詞 下個狀態(tài)。4.2.2 例子 為了具體說明怎樣用有窮狀態(tài)機(jī)技術(shù)表達(dá)系統(tǒng)的規(guī)格說明，現(xiàn)在用這種技術(shù)給出大家熟悉的電梯系統(tǒng)的規(guī)格說明。首先給出用自然語言描述的對電梯系統(tǒng)的需求：在一幢m層的大廈中需要一套控制n部電梯的產(chǎn)品，要求這n部電梯按照約束條件 C1，C2和C3在樓層間移動。C1：每部電梯內(nèi)有m個按鈕，每

14、個按鈕代表一個樓層。當(dāng)按下一個按鈕時該按鈕指示燈亮，同時電梯駛向相應(yīng)的樓層，到達(dá)按鈕指定的樓層時指示燈熄滅。C2：除了大廈的最低層和最高層之外，每層樓都有兩個按鈕分別請求電梯上行和下行。這兩個按鈕之一被按下時相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時燈熄滅。電梯向要求的方向移動。C3：當(dāng)對電梯沒有請求時，它關(guān)門并停在當(dāng)前樓層?，F(xiàn)在使用一個擴(kuò)展的有窮狀態(tài)機(jī)對本產(chǎn)品進(jìn)行規(guī)格說明。這個問題中有兩個按鈕集。N部電梯中的每一部都有m個按鈕，一個按鈕對應(yīng)一個樓層。因?yàn)檫@mn個按鈕都在電梯中，所以稱它們?yōu)殡娞莅粹o。此外，每層樓有兩個按鈕，一人請求向上，另一個請求向下，這些按鈕稱為樓層按鈕。電梯按鈕的狀態(tài)轉(zhuǎn)換如圖4.

15、2所示。令EB（）表示按下電梯內(nèi)的按鈕并請求到層去。EB（）有兩個狀態(tài)，分別是按鈕發(fā)光（打開）和不發(fā)光（關(guān)閉）。更精確地說，狀態(tài)是：EBON()：電梯按鈕 （） 打開 EBOFF()：電梯按鈕() 關(guān)閉EAF()EBON()EBP()EBOFF()圖 4.2 電梯按鈕的狀態(tài)轉(zhuǎn)換圖如果電梯按鈕 () 發(fā)光且電梯到達(dá) 層，該按鈕將熄滅。相反如果按鈕熄滅，則按下它時，按鈕將發(fā)光。上述描述中包含了兩個事件，它們分別是：EBP() ：電梯按鈕 （) 被按下EAF()：電梯 到達(dá) 層為了定義與這些事件和狀態(tài)相了解的狀態(tài)轉(zhuǎn)換規(guī)則，需要一個謂詞 ，它的含義如下：如果電梯按鈕() 處于關(guān)閉狀態(tài)當(dāng)前狀態(tài)，而且電梯

16、按鈕 () 被按下事件，而且電梯 不在 層謂詞，則該電梯按鈕打開發(fā)光下個狀態(tài)。狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下：反之，如果電梯到達(dá) 層，而且電梯按鈕是打開的，于是它就會熄滅。這條轉(zhuǎn)換規(guī)則可以形式化地表示為：接下來考慮樓層按鈕。令 表示 層請求電梯向 方向運(yùn)動的按鈕，樓層按鈕 的狀態(tài)轉(zhuǎn)換圖如圖4.3 所示。樓層按鈕的狀態(tài)如下圖 4.3 樓層按鈕的狀態(tài)轉(zhuǎn)換圖：樓層按鈕 打開：樓層按鈕 關(guān)閉如果樓層按鈕已經(jīng)打開，而且一部電梯到達(dá) 層，則按鈕關(guān)閉。反之，如果樓層按鈕原來是關(guān)閉的，被按下后該按鈕將打開。這段敘述中包含了以下兩個事件。：樓層按鈕 被子按下：電梯1或或到達(dá)層其中1表示或?yàn)?或?yàn)?或?yàn)闉榱硕x與這

17、些事件和狀態(tài)相了解的狀態(tài)轉(zhuǎn)換規(guī)則，同樣也需要一個謂詞，它是 ， 它的定義如下。：電梯停在層并且移動方向由確定為向上 或向下 或待定 。這個謂詞實(shí)際上是一個狀態(tài)，形式化方法允許把事件和狀態(tài)作為謂詞對待。使用謂詞：其中，。也就是說，如果在層請求電梯向 方向運(yùn)動的樓層按鈕處于關(guān)閉狀態(tài)，現(xiàn)在該按鈕被按下，并且當(dāng)時沒有正停在 層準(zhǔn)備向 方向移動的電梯，則該樓層按鈕打開。反之，如果樓層按鈕已經(jīng)打開，且至少有一部電梯到達(dá) 層，該部電梯將朝 方向運(yùn)動，則按鈕將關(guān)閉。在討論電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時定義的謂詞 ，可以用謂詞 重新定義如下：定義電梯按鈕和樓層按鈕的狀態(tài)都是很簡單、直觀的事情?，F(xiàn)在轉(zhuǎn)向討論電梯的狀態(tài)及其

18、轉(zhuǎn)換規(guī)則，就會出現(xiàn)一些復(fù)雜的情況。一個電梯狀態(tài)實(shí)質(zhì)上包含許多子狀態(tài)（例如，電梯減速，停止，開門，在一段時間后自動關(guān)門）。下面定義電梯的3個狀態(tài)：電梯 正沿 方向移動，即將到達(dá)的是第 層：電梯停在 層，將朝 方向移動（尚未關(guān)門）：電梯在 層等待（已關(guān)門）其中 狀態(tài)已在討論樓層按鈕時定義過，但是，現(xiàn)在的定義更完備些。圖4.4是電梯的狀態(tài)轉(zhuǎn)換圖。注意，3 個電梯停止?fàn)顟B(tài) 、 和 已被組合成一個大的狀態(tài)，這樣做的目的是減少狀態(tài)總數(shù)以簡化流圖。圖4.4中包含了下述3個可觸發(fā)狀態(tài)發(fā)生改變的事件。：電梯在樓層 關(guān)上門：電梯 靠近 層時觸發(fā)傳感口器，電梯控制器決定在當(dāng)前樓層電梯是否停下：電梯按鈕或樓層被按下打

19、開狀態(tài)，登錄需求最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則，為簡單起見，這里給出的規(guī)則僅發(fā)生在關(guān)門之時.。第一條規(guī)則表明，如果電梯 停在 層準(zhǔn)備向上移動，且門已經(jīng)關(guān)閉，則電梯將向上一樓層移動。第二條和第三者規(guī)則，分別對應(yīng)于電梯即將下降或者沒有待處理的請求的情況M ( D,e,f ) M (U, e, f+1) ST(e,f) DC(e,f) S ( D, e , f ) S ( N, e, f )S ( U, e, f )RL DC(e,f) DC(e,f) W ( e , f ) RL ST(e,f) RL M ( D,e,f-1 ) M ( U , e , f )圖 4.4 電梯的狀態(tài)轉(zhuǎn)換圖4.2.3

20、評價有窮狀態(tài)機(jī)方法采用了一種簡單的格式來描述規(guī)格說明：當(dāng)前狀態(tài)+事件+謂詞 下個狀態(tài)這種形式的規(guī)格說明易于書寫，易于驗(yàn)證，而且可以比較容易地把它轉(zhuǎn)變成設(shè)計(jì)或程序代碼，事實(shí)上，可以開發(fā)一個CASE工具把一個有窮狀態(tài)機(jī)規(guī)格說明直接轉(zhuǎn)變成源代碼。維護(hù)可以通過重新轉(zhuǎn)變來實(shí)現(xiàn)，也說是說，如果需要一個新的狀態(tài)或事件，首先修改規(guī)格說明，然后直接由新的規(guī)格說明生成新版本的產(chǎn)品。有窮狀態(tài)機(jī)方法比數(shù)據(jù)流圖技術(shù)更精確，而且和它一樣易于理解，不過，它也有缺點(diǎn)，在開發(fā)一個大系統(tǒng)時三元組（即狀態(tài)，事件，謂詞）的數(shù)量會迅速增長，此外，和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機(jī)方法也沒有處理定時需求。下節(jié)將介紹的Petri 網(wǎng)技

21、術(shù)，是一種可處理定時的問題形式方法。4.3 Petri網(wǎng)4.3.1 概念并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題。這個問題可以表現(xiàn)為多種形式，如同步問題，競爭條件以及死鎖問題。定時問題通常是由不好的設(shè)計(jì)或有錯誤的實(shí)現(xiàn)引起的，而這樣的設(shè)計(jì)或?qū)崿F(xiàn)通常又是由不好的規(guī)格說明造成。如果規(guī)格說明不恰當(dāng)，則有導(dǎo)致不完善的設(shè)計(jì)或?qū)崿F(xiàn)的危險。用于確定系統(tǒng)中隱含的定時問題的一種有效技術(shù)是Petri網(wǎng)，這種技術(shù)的一個很大的優(yōu)點(diǎn)是它也可以用于設(shè)計(jì)中。Petri網(wǎng)是由 Carl Adam Petri發(fā)明的。最初只有自動化專家對Petri網(wǎng)感興趣，后來Petri網(wǎng)在計(jì)算機(jī)科學(xué)中也得到廣泛的應(yīng)用，例如，在性能評價，操作系統(tǒng)和

22、軟件工程等頷域，etri網(wǎng)應(yīng)用得都比較廣泛。特別是已經(jīng)證明，用Petri網(wǎng)可以有效地描述并發(fā)活動。Petri網(wǎng)包含4種元素：一組位置P，一組轉(zhuǎn)換T，輸入函數(shù)I以及輸出函數(shù)O。圖4.5舉例說明了Petri網(wǎng)的組成。其中，一組位置P為 1,2,3,4, 在圖中用圓圈代表位置。一組轉(zhuǎn)換T為 1，2 ，在圖中用短直線表示轉(zhuǎn)換。 21 p4 圖 4.5 Petri 網(wǎng)的組成兩個用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭表示，它們是：1）=2，42，）=2兩個用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭表示，它們是：1）=12）=3，3注意，輸出函數(shù)2）中有兩個3,是因?yàn)橛袃蓚€箭頭由2指向3. 更形式化的P

23、etri網(wǎng)結(jié)構(gòu)，是一個四元組。 其中， 1，是一個有窮位置集，。 1，是一個有窮轉(zhuǎn)換集，且。：為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組（）的映射。：為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射。 一個無序單位組或多重組是允許一個元素有多個實(shí)例的廣義集。Petri網(wǎng)的標(biāo)記是在Petri網(wǎng)中權(quán)標(biāo)（token）的分配。例如，在圖4.6中有4個權(quán)標(biāo)，其中一個在 中，兩個在 中，中沒有，還有一個在 中。上述標(biāo)記可以用向量 （1，2，0，1） 表示。由于 和 中有權(quán)標(biāo)，因此 1啟動（即被激發(fā)）。通常，當(dāng)每當(dāng)個輸入位置所擁有的權(quán)標(biāo)數(shù)大于等于從該位置到轉(zhuǎn)換的線數(shù)時，就允許轉(zhuǎn)換。當(dāng) 被激發(fā)時， 和上各有一個權(quán)標(biāo)被移出

24、，而 上則增加一個權(quán)標(biāo)，Petri網(wǎng)中權(quán)標(biāo)總數(shù)不是固定的，在這個例子中兩個權(quán)標(biāo)被移出，而 上只有能增加一個權(quán)標(biāo)。在圖4.6中 上有權(quán)標(biāo)，因此 也可以被激發(fā)。當(dāng) 被激發(fā)時，上將移走一個權(quán)標(biāo)，而 上新增加兩個權(quán)標(biāo)，Petri網(wǎng)具有非確定性，也就是說，如果數(shù)個轉(zhuǎn)換都達(dá)到了激發(fā)條件，則其中任意一個都可以被子激發(fā)。圖4.6所示，Petri網(wǎng)標(biāo)記為（1，2，0，1）， 和 都可以 被激發(fā)。假設(shè) 被激發(fā)了，則結(jié)果如圖4.7所示，標(biāo)記，標(biāo)記為（2，1，0，0）。此時，只有 可以被激發(fā)。如果 也被激發(fā)了，則權(quán)標(biāo)從 中移出，兩個新權(quán)標(biāo)被放在 上，結(jié)果如圖4.8所示，標(biāo)記為（2，0，2，0）。. . . 圖4.6

25、帶標(biāo)記的 Petri 網(wǎng) . . . 圖4.7 圖4.6 的Petri 網(wǎng)的轉(zhuǎn)換更形式化地說，Petri網(wǎng) 中的標(biāo)記 ，是 由一組位置 到一組非負(fù)整數(shù)的映射：這樣，帶有標(biāo)記的Petri網(wǎng)成為一個五元組（ ）。對Petri網(wǎng)的一個重要擴(kuò)充是加入禁止線。如圖4.9所示，禁止線是用一個小圓圈而不是用箭頭標(biāo)記的輸入線。通常，當(dāng)每個輸入線上至少有一個權(quán)標(biāo)，而禁止線上沒有權(quán)標(biāo)的時候，相應(yīng)的轉(zhuǎn)換才是允許的。在圖4.9中，上有一個權(quán)標(biāo)而上沒有權(quán)標(biāo)，因此轉(zhuǎn)換 1可以被激發(fā)。 . . . . . 圖4.8 圖4.7 的Petri 網(wǎng)在轉(zhuǎn)換被激發(fā)后的情況 j. 圖4.9 含禁止線的 Petri 網(wǎng)4.3.2 例子

26、現(xiàn)在把Petri網(wǎng)應(yīng)用于上一節(jié)討論過的電梯問題。當(dāng)用Petri網(wǎng)表示電梯系統(tǒng)的規(guī)格說明時，每個樓層用一個位置 代表 (1) ,在Petri網(wǎng)中電梯是用一個權(quán)標(biāo)代表的。在位置 上有權(quán)標(biāo)，表示在樓層 上有電梯。1.電梯按鈕電梯問題的第一約束條件描述了電梯按鈕的行為，現(xiàn)在復(fù)述一下這個約束條件。第一條約束 ：每部電梯有m個按鈕，每層對應(yīng)一個按鈕。當(dāng)按下一個按鈕時該按鈕指示燈亮，指示電梯移往相應(yīng)的樓層。當(dāng)電梯到達(dá)指定的樓層時，按鈕將熄滅。為了用Petri網(wǎng)表達(dá)電梯按鈕的規(guī)格說明，在Petri網(wǎng)中還必須設(shè)置其它的位置。電梯中樓層的按鈕，在Petri網(wǎng)中用位置表示(1)。在上有一個權(quán)標(biāo)，就表示電梯內(nèi)樓層的按

27、鈕被按下了。電梯按鈕只有在第一次被按下時才會由暗變亮，以后再按它則只會被忽略。圖4,10所示的Petri網(wǎng)準(zhǔn)確地描述了電梯按鈕的行為規(guī)律。首先，假設(shè)按鈕沒有發(fā)亮，顯然在位置 上沒有權(quán)標(biāo)，從而在存在禁止線的情況下，轉(zhuǎn)換“ 被按下”是允許發(fā)生的，假設(shè)現(xiàn)在按下按鈕，則轉(zhuǎn)換被激發(fā)并在 上放置了一個權(quán)標(biāo)，如圖4.10所示。以后不論再按下多少次按鈕，禁止線與現(xiàn)有權(quán)標(biāo)的組合都決定了轉(zhuǎn)換 “被按下” 不能再被激發(fā)了，因此，位置 上的權(quán)標(biāo)數(shù)不會多于1。 圖 4.10 Petri 網(wǎng)表示的電梯按鈕假設(shè)電梯由 層駛向 層，因?yàn)殡娞菰?層，如圖4.10所示，位置 上有一個權(quán)標(biāo)。由于每條輸入線上各有一個權(quán)標(biāo)，轉(zhuǎn)換“電梯

28、在運(yùn)行”被激發(fā)，從而 和 上的權(quán)標(biāo)被移走，按鈕 被關(guān)閉，在位置 上出現(xiàn)一個新權(quán)標(biāo)，即轉(zhuǎn)換的激發(fā)使電梯由 層駛到 層。事實(shí)上，電梯由 層移到 層是需要時間的。為處理這個情況及其他類似的問題（例如，由于物理上的原因按鈕被按下后不能馬上發(fā)亮），Petri網(wǎng)模型中必須加入時限。也就是說，在標(biāo)準(zhǔn)Petri網(wǎng)中轉(zhuǎn)換是瞬間完成的，而在現(xiàn)實(shí)情況下就需要時間控制Petri網(wǎng)，以使轉(zhuǎn)換與非零時間相了解。2.樓層按鈕在第二個約束條件中描述了樓層按鈕的行為。第二條約束： 除了第一層與頂層之外，每個樓臺層都有兩個按鈕，一個要求電梯上行，另一個要求電梯下行，這些按鈕在按下時發(fā)亮，當(dāng)電梯到達(dá)該層并將向指定方向移動時，相應(yīng)的

29、按鈕才什么熄滅。在Petri網(wǎng)中樓層按鈕用位置和 和表示，分別代表 樓層請求電梯上行和下行的按鈕。底層的按鈕為 ,最高層的按鈕為 ,中間每一層有兩個按鈕 和（1<<）. 圖4.11所示的情況為電梯由 層駛向 層，根據(jù)電梯乖客的要求，某一個樓層按鈕亮或兩個樓層按鈕都亮。如果兩個按鈕都亮了，則只有一個按鈕熄滅。圖4.11所示的Petri網(wǎng)可以保證，當(dāng)兩個按鈕都亮了時候，只有一個按鈕熄滅。但是要保證按鈕熄滅正確，則需要更復(fù)雜的Petri網(wǎng)網(wǎng)模型，對此本書不做更進(jìn)一步的介紹。圖 4.11 Petri 網(wǎng)表示樓層按鈕 最后，考慮第三條約束。第三條約束 ： 當(dāng)電梯沒有收到請求時，它將停留在當(dāng)前

30、樓層并關(guān)門。這條約束很容易實(shí)，如圖4.11所示，當(dāng)沒有請求(和上無權(quán)標(biāo)）時，任何一個轉(zhuǎn)換“電梯在運(yùn)行”都不能被激發(fā)。4.4 Z語言 在形式化的規(guī)格說明語言中，Z語言贏得了廣泛的贊譽(yù)。使用Z語言需要具備集合論、函數(shù)、數(shù)理邏輯等方面的知識。即使用戶已經(jīng)掌握了所需要的背景知識，Z語言也是相當(dāng)難學(xué)的，因?yàn)樗耸褂贸Ｓ玫募险摵蛿?shù)理邏輯符號之外，還使用一些特殊符號。4.4.1 簡介 本節(jié)結(jié)合電梯問題的例子，簡要地介紹Z語言。用Z語言描述的、最簡單的形式化規(guī)格說明含有下述4個部分： ·給定的集合、數(shù)據(jù)類型及常數(shù)。 ·狀態(tài)定義。 ·初始狀態(tài)。 ·操作。 現(xiàn)在依次介紹

31、這4個部分。1. 給定的集合 一個Z規(guī)格說明從一系列給定的初始化集合開始。所謂初始化集合就是不需要詳細(xì)定義的集合，這種集合用帶方括號的形式表示。對于電梯問題，給定的初始化集合稱為Button，即所有按鈕的集合，因此，Z規(guī)格說明開始于： Button2. 狀態(tài)定義 一個Z規(guī)格說明由若干個“格(schema)”組成，每個格含有一組變量說明和一系列限定變量取值范圍的謂詞。例如，格S的格式如圖412所示。 在電梯問題中，Button有4個子集，即floor_buttons(樓層按鈕的集合)、elevator_buttons(電梯按鈕的集合)、buttons(電梯問題中所有按鈕的集合)以及pushed(

32、所有被按的按鈕的集合，即所有處于打開狀態(tài)的按鈕的集合)。圖413描述了格Button_State，其中，符號P表示冪集(即給定集的所有子集)。約束條件聲明，floor_buttons集與elevator_buttons集不相交，而且它們共同組成buttons集(在下面的討論中并不需要floor_buttons集和elevator_buttons集，把它們放于圖413中只是用來說明Z格包含的內(nèi)容)。 S floor_butons,elevator_button: P Button butons : P Button pushed : P Buton Button_State 說明 謂詞 floo

33、r_buttonselevator_buttons= floor_buttonselevator_buttons=buttons 圖 4.13 Z 格 Button_State圖 4.12 Z 格 S的格式3.初始狀態(tài) 抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。對于電梯問題來說，抽象的初始狀態(tài)為： ， Button_InitButton_State pushed=上式表示，當(dāng)系統(tǒng)首次開啟時pushed集為空，即所有按鈕都處于關(guān)閉狀態(tài)。4.操作 如果一個原來處于關(guān)閉狀態(tài)的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到pushed集中。圖414定義了操作Push_Button(按按鈕)。Z語言的語法

34、規(guī)定，當(dāng)一個格被用在另一個格中時，要在它的前面加上三角形符號作為前綴，因此，格Push_Button的第一行最前面有一個三角形符號作為格Button_State的前綴。操作Push_Button有一個輸入變量“button?"。問號“?”表示輸入變量，而感嘆號“!”代表輸出變量。 Push_Button Button_Statebutton? : Button ( button?buttons) ( button? pushed)(pushed= pushed button?)(button? pushed)( pushed= pushed ) ) )圖414操作Push_Butto

35、n的Z規(guī)格說明 操作的謂詞部分，包含了一組調(diào)用操作的前置條件，以及操作完全結(jié)束后的后置條件。如果前置條件成立，則操作執(zhí)行完成后可得到后置條件。但是，如果在前置條件不成立的情況下調(diào)用該操作，則不能得到指定的結(jié)果(因此結(jié)果無法預(yù)測)。 圖414中的第一個前置條件規(guī)定，“button?"必須是buttons的一個元素，而buttons是電梯系統(tǒng)中所有按鈕的集合。如果第二個前置條件button? pushed得到滿足(即按鈕沒有開啟)，則更新pushed按鈕集，使之包含剛開啟的按鈕"button?"。在Z語言中，當(dāng)一個變量的值發(fā)生改變時，就用符號 “ ”表示。也就是說，后

36、置條件是當(dāng)執(zhí)行完操作Push_Button之后，“button?”將被加入到pushed集中。無需直接打開按鈕，只要使“button?"變成pushed中的一個元素即可。 還有一種可能性是，被按的按鈕原先已經(jīng)打開了。由于button?pushed，根據(jù)第三個前置條件，將沒有任何事情發(fā)生，這可以用pushed = pushed來表示，即pushed的新狀態(tài)和舊狀態(tài)一樣。注意，如果沒有第三個前置條件，規(guī)格說明將不能說明在一個按鈕已被按過之后又被按了一次的情況下將發(fā)生什么事，因此，結(jié)果將是不可預(yù)測的。 假設(shè)電梯到達(dá)了某樓層，如果相應(yīng)的樓層按鈕已經(jīng)打開，則此時它會關(guān)閉；同樣，如果相應(yīng)的電梯按

37、鈕已經(jīng)打開，則此時它也會關(guān)閉。也就是說，如果“button?"屬于pushed集，則將它移出該集合，如圖415所示(符號“”表示集合差運(yùn)算)。但是，如果按鈕“button?”原先沒有打開，則pushed集合不發(fā)生變化。 Floor_Arrival Button_Statebutton? : Button ( button?buttons) ( button?pushed)(pushed= pushed button?)(button? pushed)( pushed= pushed ) ) ) 圖415操作Floor_Arrival的z規(guī)格說明本節(jié)的討論有所簡化，沒有區(qū)分上行和下行樓

38、層按鈕，但是，仍然講清了使用Z語言說明電梯問題中按鈕狀態(tài)的方法。4.4.2 評價 已經(jīng)在許多軟件開發(fā)項(xiàng)目中成功地運(yùn)用了Z語言，目前，Z也許是應(yīng)用得最廣泛的形式化語言，尤其是在大型項(xiàng)目中Z語言的優(yōu)勢更加明顯。Z語言之所以會獲得如此多的成功，主要有以下幾個原因： (1)可以比較容易地發(fā)現(xiàn)用Z寫的規(guī)格說明的錯誤，特別是在自己審查規(guī)格說明，及根據(jù)形式化的規(guī)格說明來審查設(shè)計(jì)與代碼時，情況更是如此。 (2)用Z寫規(guī)格說明時，要求整理十分精確地使用Z說明符。由于對精確性的要求很高，從而和非形式化規(guī)格說明相比，減少了模糊性、不一致性和遺漏。 (3)Z是一種形式化語言，在需要時開發(fā)者可以嚴(yán)格地驗(yàn)證規(guī)格說明的正確

39、性。 (4)雖然完全學(xué)會Z語言相當(dāng)困難，但是，經(jīng)驗(yàn)表明，只學(xué)過中學(xué)數(shù)學(xué)的軟件開發(fā)人員仍然可以只用比較短的時間就學(xué)會編寫Z規(guī)格說明，當(dāng)然，這些人還沒有能力證明規(guī)格說明的結(jié)果是否正確。 (5)使用Z語言可以降低軟件開發(fā)費(fèi)用。雖然用Z寫規(guī)格說明所需用的時間比使用非形式化技術(shù)要多，但開發(fā)過程所需要的總時間卻減少了。 (6)雖然用戶無法理解用Z寫的規(guī)格說明，但是，可以依據(jù)Z規(guī)格說明用自然語言重寫規(guī)格說明。經(jīng)驗(yàn)證明，這樣得到的自然語言規(guī)格說明，比直接用自然語言寫出的非形式化規(guī)格說明更清楚、更正確。 使用形式化規(guī)格說明是全球的總趨勢，過去，主要是歐洲習(xí)慣于使用形式化規(guī)格說明技術(shù)，現(xiàn)在越來越多的美國公司也開始使用形式化規(guī)格說明技術(shù)。4.5 小 結(jié) 基于數(shù)學(xué)的形式化規(guī)格說明技術(shù)，目前還沒有在軟件產(chǎn)業(yè)界廣泛應(yīng)用，但是，與欠形式化的方法比較起來，它確實(shí)有實(shí)質(zhì)性的優(yōu)點(diǎn)：形式化的規(guī)格說明可以用數(shù)學(xué)方法研究、驗(yàn)證(例如，一個正確的程序可以被證明滿足其規(guī)格說明，兩個規(guī)格說明可以被證明是等價的，規(guī)格說明中存在的某些形式的