1、第4章 形式化說明技術,4.1 概述 4.2 有窮狀態(tài)機 4.3 Petri網 4.4 Z語言 4.5 小結 習題,按照形式化的程度，可以把軟件工程使用的方法劃分成非形式化、半形式化和形式化3類。用自然語言描述需求規(guī)格說明，是典型的非形式化方法。用數據流圖或實體-聯(lián)系圖建立模型，是典型的半形式化方法。 所謂形式化方法，是描述系統(tǒng)性質的基于數學的技術，也就是說，如果一種方法有堅實的數學基礎，那么它就是形式化的。,用自然語言書寫的系統(tǒng)規(guī)格說明書，可能存在矛盾、二義性、含糊性、不完整性及抽象層次混亂等問題。 所謂矛盾是指一組相互沖突的陳述。 二義性是指讀者可以用不同方式理解的陳述。,4.1 概述 4

2、.1.1 非形式化方法的缺點,系統(tǒng)規(guī)格說明書是很龐大的文檔，因此，幾乎不可避免地會出現含糊性。實際上，這樣籠統(tǒng)的陳述并沒有給出任何有用的信息。 不完整性可能是在系統(tǒng)規(guī)格說明中最常遇到的問題之一。 抽象層次混亂是指在非常抽象的陳述中混進了一些關于細節(jié)的低層次陳述。這樣的規(guī)格說明書使得讀者很難了解系統(tǒng)的整體功能結構。,數學最有用的一個性質是，它能夠簡潔準確地描述物理現象、對象或動作的結果，因此是理想的建模工具。數學特別適合于表示狀態(tài)，也就是表示“做什么”。,4.1.2 形式化方法的優(yōu)點,在軟件開發(fā)過程中使用數學的另一個優(yōu)點是，可以在不同的軟件工程活動之間平滑地過渡。不僅功能規(guī)格說明，而且系統(tǒng)設計也

3、可以用數學表達，當然，程序代碼也是一種數學符號(雖然是一種相當繁瑣、冗長的數學符號)。 數學作為軟件開發(fā)工具的最后一個優(yōu)點是，它提供了高層確認的手段?？梢允褂脭祵W方法證明，設計符合規(guī)格說明，程序代碼正確地實現了設計結果。,(1) 應該選用適當的表示方法。 (2) 應該形式化，但不要過分形式化。 (3) 應該估算成本。 (4) 應該有形式化方法顧問隨時提供咨詢。 (5) 不應該放棄傳統(tǒng)的開發(fā)方法。 (6) 應該建立詳盡的文檔。 (7) 不應該放棄質量標準。 (8) 不應該盲目依賴形式化方法。 (9) 應該測試、測試再測試。 (10) 應該重用。,4.1.3 應用形式化方法的準則,下面通過一個簡單

4、例子介紹有窮狀態(tài)機的基本概念。 一個保險箱上裝了一個復合鎖，鎖有三個位置，分別標記為1、2、3，轉盤可向左(L)或向右(R)轉動。這樣，在任意時刻轉盤都有6種可能的運動，即1L、1R、2L、2R、3L和3R。保險箱的組合密碼是1L、3R、2L，轉盤的任何其他運動都將引起報警。圖4.1描繪了保險箱的狀態(tài)轉換情況。,4.2 有窮狀態(tài)機 4.2.1 概念,圖4.1 保險箱的狀態(tài)轉換圖,圖4.1是一個有窮狀態(tài)機的狀態(tài)轉換圖。狀態(tài)轉換并不一定要用圖形方式描述，表4.1（見書68頁）的表格形式也可以表達同樣的信息。 從上面這個簡單例子可以看出，一個有窮狀態(tài)機包括下述5個部分：狀態(tài)集J、輸入集K、由當前狀態(tài)

5、和當前輸入確定下一個狀態(tài)(次態(tài))的轉換函數T、初始態(tài)S和終態(tài)集F。對于保險箱的例子，相應的有窮狀態(tài)機的各部分如下。 狀態(tài)集J：保險箱鎖定，A，B，保險箱解鎖，報警。 輸入集K：1L，1R，2L，2R，3L，3R。,轉換函數T：如表4.1所示。 初始態(tài)S：保險箱鎖定。 終態(tài)集F：保險箱解鎖，報警。 如果使用更形式化的術語，一個有窮狀態(tài)機可以表示為一個5元組(J，K，T，S，F)，其中： J是一個有窮的非空狀態(tài)集； K是一個有窮的非空輸入集； T是一個從(J-F)K到J的轉換函數； SJ，是一個初始狀態(tài)； FJ，是終態(tài)集。,有窮狀態(tài)機的概念在計算機系統(tǒng)中應用得非常廣泛。例如，每個菜單驅動的用戶界面

6、都是一個有窮狀態(tài)機的實現。一個菜單的顯示和一個狀態(tài)相對應，鍵盤輸入或用鼠標選擇一個圖標是使系統(tǒng)進入其他狀態(tài)的一個事件。狀態(tài)的每個轉換都具有下面的形式： 當前狀態(tài)菜單+事件所選擇的項下個狀態(tài)。,為了對一個系統(tǒng)進行規(guī)格說明，通常都需要對有窮狀態(tài)機做一個很有用的擴展，即在前述的5元組中加入第6個組件謂詞集P，從而把有窮狀態(tài)機擴展為一個6元組，其中每個謂詞都是系統(tǒng)全局狀態(tài)Y的函數。轉換函數T現在是一個從(J-F)KP到J的函數?，F在的轉換規(guī)則形式如下： 當前狀態(tài)菜單+事件所選擇的項+謂詞下個狀態(tài)。,有限狀態(tài)自動機（FSM finite state machine 或者FSA finite state

7、automaton ）是為研究有限內存的計算過程和某些語言類而抽象出的一種計算模型。有限狀態(tài)自動機擁有有限數量的狀態(tài)，每個狀態(tài)可以遷移到零個或多個狀態(tài)，輸入字串決定執(zhí)行哪個狀態(tài)的遷移。有限狀態(tài)自動機可以表示為一個有向圖。有限狀態(tài)自動機是自動機理論的研究對象。 有多種類型的有限狀態(tài)自動機：接受器判斷是否接受輸入；轉換器對給定輸入產生一個輸出。常見的轉換器有 Moore 機 與 Mealy 機。Moore 機對每一個狀態(tài)都附加有輸出動作，Mealy 機對每一個轉移都附加有輸出動作。,為了具體說明怎樣用有窮狀態(tài)機技術表達系統(tǒng)的規(guī)格說明，現在用這種技術給出大家熟悉的電梯系統(tǒng)的規(guī)格說明。首先給出用自然語

8、言描述的對電梯系統(tǒng)的需求： 在一幢m層的大廈中需要一套控制n部電梯的產品，要求這n部電梯按照約束條件C1，C2和C3在樓層間移動。 C1：每部電梯內有m個按鈕，每個按鈕代表一個樓層。當按下一個按鈕時該按鈕指示燈亮，同時電梯駛向相應的樓層，到達按鈕指定的樓層時指示燈熄滅。,4.2.2 例子,C2：除了大廈的最低層和最高層之外，每層樓都有兩個按鈕分別請求電梯上行和下行。這兩個按鈕之一被按下時相應的指示燈亮，當電梯到達此樓層時燈熄滅，電梯向要求的方向移動。 C3：當對電梯沒有請求時，它關門并停在當前樓層。 現在使用一個擴展的有窮狀態(tài)機對本產品進行規(guī)格說明。這個問題中有兩個按鈕集。n部電梯中的每一部都

9、有m個按鈕，一個按鈕對應一個樓層。因為這mn個按鈕都在電梯中，所以稱它們?yōu)殡娞莅粹o。此外，每層樓有兩個按鈕，一個請求向上，另一個請求向下，這些按鈕稱為樓層按鈕。,電梯按鈕的狀態(tài)轉換圖如圖4.2所示。令EB(e,f)表示按下電梯e內的按鈕并請求到f層去。EB(e,f)有兩個狀態(tài)，分別是按鈕發(fā)光(打開)和不發(fā)光(關閉)。更精確地說，狀態(tài)是： EBON(e,f)：電梯按鈕(e,f)打開 EBOFF(e,f)：電梯按鈕(e,f)關閉 如果電梯按鈕(e,f)發(fā)光且電梯到達f層，該按鈕將熄滅。相反如果按鈕熄滅，則按下它時，按鈕將發(fā)光。上述描述中包含了兩個事件，它們分別是： EBP(e,f)：電梯按鈕(e,

10、f)被按下 EAF(e,f)：電梯e到達f層,圖4.2 電梯按鈕的狀態(tài)轉換圖 圖4.3樓層按鈕的狀態(tài)轉換圖,為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉換規(guī)則，需要一個謂詞V(e,f)，它的含義如下： V(e,f)：電梯e停在f層 如果電梯按鈕(e,f)處于關閉狀態(tài)當前狀態(tài)，而且電梯按鈕(e,f)被按下事件，而且電梯e不在f層謂詞，則該電梯按鈕打開發(fā)光下個狀態(tài)。狀態(tài)轉換規(guī)則的形式化描述如下： EBOFF(e,f)+EBP(e,f)+not V(e,f)EBON(e,f) 反之，如果電梯到達f層，而且電梯按鈕是打開的，于是它就會熄滅。這條轉換規(guī)則可以形式化地表示為： EBON(e,f)+EAF(e,f

11、)EBOFF(e,f),接下來考慮樓層按鈕。令FB(d,f)表示f層請求電梯向d方向運動的按鈕，樓層按鈕FB(d,f)的狀態(tài)轉換圖如圖4.3所示。 樓層按鈕的狀態(tài)如下： FBON(d,f)：樓層按鈕(d,f)打開 FBOFF(d,f)：樓層按鈕(d,f)關閉 如果樓層按鈕已經打開，而且一部電梯到達f層，則按鈕關閉。反之，如果樓層按鈕原來是關閉的，被按下后該按鈕將打開。這段敘述中包含了以下兩個事件。,FBP(d,f)：樓層按鈕(d,f)被按下 EAF(1n,f)：電梯1或或n到達f層 其中1n表示或為1或為2或為n。 為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉換規(guī)則，同樣也需要一個謂詞，它是S(d,

12、e,f)，它的定義如下。 S(d,e,f)：電梯e停在f層并且移動方向由d確定為向上(d=U)或向下(d=D)或待定(d=N)。 這個謂詞實際上是一個狀態(tài)，形式化方法允許把事件和狀態(tài)作為謂詞對待。,使用謂詞S(d,e,f)，形式化轉換規(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=UorDor N。 也就是說，如果在f層請求電梯向d方向運動的樓層按鈕處于關閉狀態(tài)，現在該按鈕被按下，并且當時沒有正停在f層準備向d方向移動的電梯，則該樓層按鈕打開。反之，如果樓層

13、按鈕已經打開，且至少有一部電梯到達f層，該部電梯將朝d方向運動，則按鈕將關閉。,現在轉向討論電梯的狀態(tài)及其轉換規(guī)則，就會出現一些復雜的情況。一個電梯狀態(tài)實質上包含許多子狀態(tài)。 下面定義電梯的3個狀態(tài)： M(d,e,f)：電梯e正沿d方向移動，即將到達的是第f層 S(d,e,f)：電梯e停在f層，將朝d方向移動(尚未關門) W(e,f)：電梯e在f層等待(已關門),其中S(d,e,f)狀態(tài)已在討論樓層按鈕時定義過，但是，現在的定義更完備一些。 圖4.4是電梯的狀態(tài)轉換圖。3個電梯停止狀態(tài)S(U,e,f)、S(N,e,f)和S(D,e,f)已被組合成一個大的狀態(tài)，這樣做的目的是減少狀態(tài)總數以簡化流

14、圖。 圖4.4中包含了下述3個可觸發(fā)狀態(tài)發(fā)生改變的事件。 DC(e,f)：電梯e在樓層f關上門 ST(e,f)：電梯e靠近f層時觸發(fā)傳感器，電梯控制器決定在當前樓層電梯是否停下 RL：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)，登錄需求,圖4.4 電梯的狀態(tài)轉換圖,最后，給出電梯的狀態(tài)轉換規(guī)則。為簡單起見，這里給出的規(guī)則僅發(fā)生在關門之時。 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ī)則表明，如果電梯e停在f層準備向上移動，且門已經關閉，則電梯將向上一樓層移動。第二條和第三條規(guī)則，分別

15、對應于電梯即將下降或者沒有待處理的請求的情況。,有窮狀態(tài)機方法采用了一種簡單的格式來描述規(guī)格說明： 當前狀態(tài)+事件+謂詞下個狀態(tài) 這種形式的規(guī)格說明易于書寫、易于驗證，而且可以比較容易地把它轉變成設計或程序代碼。 事實上，可以開發(fā)一個CASE工具把一個有窮狀態(tài)機規(guī)格說明直接轉變?yōu)樵创a。維護可以通過重新轉變來實現，也就是說，如果需要一個新的狀態(tài)或事件，首先修改規(guī)格說明，然后直接由新的規(guī)格說明生成新版本的產品。,4.2.3 評價,有窮狀態(tài)機方法比數據流圖技術更精確，而且和它一樣易于理解。 缺點：在開發(fā)一個大系統(tǒng)時三元組(即狀態(tài)、事件、謂詞)的數量會迅速增長。此外，和數據流圖方法一樣，形式化的有窮

16、狀態(tài)機方法也沒有處理定時需求。下節(jié)將介紹的Petri網技術，是一種可處理定時問題的形式化方法。,并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題。這個問題可以表現為多種形式，如同步問題、競爭條件以及死鎖問題。,4.3 Petri網 4.3.1 概念,Petri網是由Carl Adam Petri發(fā)明的。最初只有自動化專家對Petri網感興趣，后來Petri網在計算機科學中也得到廣泛的應用，例如，在性能評價、操作系統(tǒng)和軟件工程等領域，Petri網應用得都比較廣泛。特別是已經證明，用Petri網可以有效地描述并發(fā)活動。 Petri網包含4種元素：一組位置P、一組轉換T、輸入函數I以及輸出函數O。圖4.5舉例

17、說明了Petri網的組成。,圖4.5 Petri網的組成,一組位置P為P1，P2，P3，P4，在圖中用圓圈代表位置。 一組轉換T為t1，t2，在圖中用短直線表示轉換。 兩個用于轉換的輸入函數，用由位置指向轉換的箭頭表示，它們是： I(t1)=P2，P4 I(t2)=P2 兩個用于轉換的輸出函數，用由轉換指向位置的箭頭表示，它們是： 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，

18、且T和P不相交。 I：TP為輸入函數，是由轉換到位置無序單位組(bags)的映射。 O：TP為輸出函數，是由轉換到位置無序單位組的映射。,Z語言中Z是指著名的數學家Zermolo,他的主要成就是集合論。 用Z語言描述的、最簡單的形式化規(guī)格說明含有下述4個部分： 給定的集合、數據類型及常數。 狀態(tài)定義。 初始狀態(tài)。 操作。,4.4 Z語言 4.4.1 簡介,1. 給定的集合 一個Z規(guī)格說明從一系列給定的初始化集合開始。所謂初始化集合就是不需要詳細定義的集合，這種集合用帶方括號的形式表示。對于電梯問題，給定的初始化集合稱為Button，即所有按鈕的集合，因此，Z規(guī)格說明開始于： Button 2.

19、 狀態(tài)定義 一個Z規(guī)格說明由若干個“格(schema)”組成，每個格含有一組變量說明和一系列限定變量取值范圍的謂詞。例如，格S的格式如圖4.12所示。,圖4.12 Z格S的格式,3. 初始狀態(tài) 抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。對于電梯問題來說，抽象的初始狀態(tài)為： Button_InitButton_Statepushed= 上式表示，當系統(tǒng)首次開啟時pushed集為空，即所有按鈕都處于關閉狀態(tài)。 4. 操作 如果一個原來處于關閉狀態(tài)的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到pushed集中。圖4.14（見書87頁）定義了操作Push_Button(按按鈕)。,已經在許多軟件開發(fā)項目中成功地運用了Z語言，目前，Z也許是應用得最廣泛的形式化語言，尤其是在大型項目中Z語言的優(yōu)勢更加明顯。Z語言之所以會獲得如此多的成功，主要有以下幾個原因： (1) 可以比較容易地發(fā)現用Z寫的規(guī)格說明的錯誤，特別是在自己審查規(guī)格說明，及根據形式化的規(guī)格說明來審查設計與代碼時，情況更是如此。 (2) 用Z寫規(guī)格說明時，要求作者十分精確地使用Z說明符。由于對精確性的要求很高，從而和非形式化規(guī)格說明相比，減少了模糊性、不一致性和遺漏。,4.4.2 評價,(3) Z是一種形式