形式化說明技術(shù).ppt

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

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

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

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

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

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

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

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

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

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

11、)EBOFF(e,f),接下來考慮樓層按鈕。令FB(d,f)表示f層請求電梯向d方向運動的按鈕，樓層按鈕FB(d,f)的狀態(tài)轉(zhuǎn)換圖如圖4.3所示。 樓層按鈕的狀態(tài)如下： FBON(d,f)：樓層按鈕(d,f)打開 FBOFF(d,f)：樓層按鈕(d,f)關(guān)閉 如果樓層按鈕已經(jīng)打開，而且一部電梯到達(dá)f層，則按鈕關(guān)閉。反之，如果樓層按鈕原來是關(guān)閉的，被按下后該按鈕將打開。這段敘述中包含了以下兩個事件。,FBP(d,f)：樓層按鈕(d,f)被按下 EAF(1n,f)：電梯1或或n到達(dá)f層 其中1n表示或為1或為2或為n。 為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(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)，形式化轉(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=UorDor N。 也就是說，如果在f層請求電梯向d方向運動的樓層按鈕處于關(guān)閉狀態(tài)，現(xiàn)在該按鈕被按下，并且當(dāng)時沒有正停在f層準(zhǔn)備向d方向移動的電梯，則該樓層按鈕打開。反之，如果樓層

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

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

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

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

17、說明了Petri網(wǎng)的組成。,圖4.5 Petri網(wǎng)的組成,一組位置P為P1，P2，P3，P4，在圖中用圓圈代表位置。 一組轉(zhuǎn)換T為t1，t2，在圖中用短直線表示轉(zhuǎn)換。 兩個用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭表示，它們是： I(t1)=P2，P4 I(t2)=P2 兩個用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭表示，它們是： O(t1)=P1 O(t2)=P3，P3,注意，輸出函數(shù)O(t2)中有兩個P3，是因為有兩個箭頭由t2指向P3。 更形式化的Petri網(wǎng)結(jié)構(gòu)，是一個四元組C=(P,T,I,O)。 其中， P=P1，Pn是一個有窮位置集，n0。 T=t1，tm是一個有窮轉(zhuǎn)換集，m0，

18、且T和P不相交。 I：TP為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組(bags)的映射。 O：TP為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射。,Z語言中Z是指著名的數(shù)學(xué)家Zermolo,他的主要成就是集合論。 用Z語言描述的、最簡單的形式化規(guī)格說明含有下述4個部分： 給定的集合、數(shù)據(jù)類型及常數(shù)。 狀態(tài)定義。 初始狀態(tài)。 操作。,4.4 Z語言 4.4.1 簡介,1. 給定的集合 一個Z規(guī)格說明從一系列給定的初始化集合開始。所謂初始化集合就是不需要詳細(xì)定義的集合，這種集合用帶方括號的形式表示。對于電梯問題，給定的初始化集合稱為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= 上式表示，當(dāng)系統(tǒng)首次開啟時pushed集為空，即所有按鈕都處于關(guān)閉狀態(tài)。 4. 操作 如果一個原來處于關(guān)閉狀態(tài)的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到pushed集中。圖4.14（見書87頁）定義了操作Push_Button(按按鈕)。,已經(jīng)在許多軟件開發(fā)項目中成功地運用了Z語言，目前，Z也許是應(yīng)用得最廣泛的形式化語言，尤其是在大型項目中Z語言的優(yōu)勢更加明顯。Z語言之所以會獲得如此多的成功，主要有以下幾個原因： (1) 可以比較容易地發(fā)現(xiàn)用Z寫的規(guī)格說明的錯誤，特別是在自己審查規(guī)格說明，及根據(jù)形式化的規(guī)格說明來審查設(shè)計與代碼時，情況更是如此。 (2) 用Z寫規(guī)格說明時，要求作者十分精確地使用Z說明符。由于對精確性的要求很高，從而和非形式化規(guī)格說明相比，減少了模糊性、不一致性和遺漏。,4.4.2 評價,(3) Z是一種形式