軟件工程第四章課件

1、2形式化方法形式化方法n是描述系統(tǒng)性質的基于是描述系統(tǒng)性質的基于的技術，的技術，有堅實的數(shù)學基礎。有堅實的數(shù)學基礎。n按照形式化的程度，劃分成非形式化、按照形式化的程度，劃分成非形式化、半形式化和形式化半形式化和形式化3類。類。u用自然語言描述需求規(guī)格說明，是典型的用自然語言描述需求規(guī)格說明，是典型的非形式化方法。非形式化方法。u用數(shù)據(jù)流圖或實體用數(shù)據(jù)流圖或實體-聯(lián)系圖建立模型，是典聯(lián)系圖建立模型，是典型的半形式化方法。型的半形式化方法。34.1.1 非形式化方法的缺點非形式化方法的缺點n自然語言書寫的規(guī)格說明書，可能存自然語言書寫的規(guī)格說明書，可能存在在44.1.2 形式化方法的優(yōu)點形式化方

2、法的優(yōu)點，是理想的建模工具，是理想的建模工具n驗證需求，以驗證需求，以n平滑過渡，也可以用于設計平滑過渡，也可以用于設計n提供了高層提供了高層的手段的手段u證明設計符合規(guī)格說明證明設計符合規(guī)格說明u證明程序代碼正確地實現(xiàn)了設計結果證明程序代碼正確地實現(xiàn)了設計結果54.1.3 應用形式化方法的準則應用形式化方法的準則(1) 應該選用適當?shù)谋硎痉椒?。應該選用適當?shù)谋硎痉椒ā?2) 應該形式化，但不要過分形式化。應該形式化，但不要過分形式化。(3) 應該估算成本。應該估算成本。(4) 應該有形式化方法顧問隨時提供咨詢。應該有形式化方法顧問隨時提供咨詢。(5) 不應該放棄傳統(tǒng)的開發(fā)方法。不應該放棄傳統(tǒng)

3、的開發(fā)方法。(6) 應該建立詳盡的文檔。應該建立詳盡的文檔。(7) 不應該放棄質量標準。不應該放棄質量標準。(8) 不應該盲目依賴形式化方法。不應該盲目依賴形式化方法。(9) 應該測試、測試再測試。應該測試、測試再測試。(10) 應該重用。應該重用。64.2 有窮狀態(tài)機有窮狀態(tài)機7進程的狀態(tài)遷移進程的狀態(tài)遷移8保險箱的狀態(tài)轉換圖保險箱的狀態(tài)轉換圖例：一個保險箱上裝了一個復合鎖，例：一個保險箱上裝了一個復合鎖，鎖有三個位置，分別標記為鎖有三個位置，分別標記為1、2、3，轉盤可向左轉盤可向左(L)或向右或向右(R)轉動。這樣，轉動。這樣，在任意時刻轉盤都有在任意時刻轉盤都有6種可能的運動，種可能的

4、運動，即即1L、1R、2L、2R、3L和和3R。保險箱。保險箱的組合密碼是的組合密碼是1L、3R、2L，轉盤的任何，轉盤的任何其他運動都將引起報警。其他運動都將引起報警。9保險箱的狀態(tài)轉換圖保險箱的狀態(tài)轉換圖10有窮狀態(tài)機的狀態(tài)轉換表有窮狀態(tài)機的狀態(tài)轉換表11有窮狀態(tài)機的表示有窮狀態(tài)機的表示n包括包括5個部分：個部分：狀態(tài)集狀態(tài)集J、輸入集輸入集K、由當前狀態(tài)、由當前狀態(tài)和當前輸入確定下一個狀態(tài)和當前輸入確定下一個狀態(tài)(次態(tài)次態(tài))的的轉換函數(shù)轉換函數(shù)T、初始態(tài)初始態(tài)S和和終態(tài)集終態(tài)集F。n保險箱的有窮狀態(tài)機：保險箱的有窮狀態(tài)機：狀態(tài)集狀態(tài)集J：保險箱鎖定，：保險箱鎖定，A，B，保險箱解鎖，報警

5、。，保險箱解鎖，報警。輸入集輸入集K：1L，1R，2L，2R，3L，3R。轉換函數(shù)轉換函數(shù)T：如表：如表4.1所示。所示。初始態(tài)初始態(tài)S：保險箱鎖定。：保險箱鎖定。終態(tài)集終態(tài)集F：保險箱解鎖，報警。：保險箱解鎖，報警。12有窮狀態(tài)機有窮狀態(tài)機5元組表示元組表示n表示為一個表示為一個5元組元組(J，K，T，S，F(xiàn))，其中：其中：J是一個有窮的非空狀態(tài)集；是一個有窮的非空狀態(tài)集；K是一個有窮的非空輸入集；是一個有窮的非空輸入集；T是一個從是一個從(J-F)K到到J的轉換函數(shù)；的轉換函數(shù)；SJ，是一個初始狀態(tài)；，是一個初始狀態(tài)；FJ，是終態(tài)集。，是終態(tài)集。 13狀態(tài)轉換表示形式狀態(tài)轉換表示形式n狀態(tài)

6、的每個轉換都具有下面的形式：狀態(tài)的每個轉換都具有下面的形式：當前狀態(tài)當前狀態(tài)菜單菜單+事件事件所選擇的項所選擇的項下下個狀態(tài)。個狀態(tài)。n加入加入謂詞集謂詞集P把有窮狀態(tài)機擴展為一個把有窮狀態(tài)機擴展為一個6元組，元組，其中每個謂詞都是系統(tǒng)全局狀態(tài)其中每個謂詞都是系統(tǒng)全局狀態(tài)Y的函數(shù)。轉的函數(shù)。轉換函數(shù)換函數(shù)T則是一個從則是一個從(J-F)KP到到J的函數(shù)。的函數(shù)。轉換規(guī)則形式如下：轉換規(guī)則形式如下：當前狀態(tài)當前狀態(tài)菜單菜單+事件事件所選擇的項所選擇的項+謂詞謂詞下個狀態(tài)。下個狀態(tài)。14電梯系統(tǒng)的需求電梯系統(tǒng)的需求n自然語言描述的對電梯系統(tǒng)的需求：自然語言描述的對電梯系統(tǒng)的需求：在一幢在一幢m層的

7、大廈中需要一套控制層的大廈中需要一套控制n部電梯的產(chǎn)品，要部電梯的產(chǎn)品，要求這求這n部電梯按照約束條件部電梯按照約束條件C1，C2和和C3在樓層間移動。在樓層間移動。C1：每部電梯內有：每部電梯內有m個按鈕，每個按鈕代表一個樓層。個按鈕，每個按鈕代表一個樓層。當按下一個按鈕時該按鈕指示燈亮，同時電梯駛向相當按下一個按鈕時該按鈕指示燈亮，同時電梯駛向相應的樓層，到達按鈕指定的樓層時指示燈熄滅。應的樓層，到達按鈕指定的樓層時指示燈熄滅。C2：除了大廈的最低層和最高層之外，每層樓都有兩：除了大廈的最低層和最高層之外，每層樓都有兩個按鈕分別請求電梯上行和下行。這兩個按鈕之一被個按鈕分別請求電梯上行和下

8、行。這兩個按鈕之一被按下時相應的指示燈亮，當電梯到達此樓層時燈熄滅，按下時相應的指示燈亮，當電梯到達此樓層時燈熄滅，電梯向要求的方向移動。電梯向要求的方向移動。C3：當對電梯沒有請求時，它關門并停在當前樓層。：當對電梯沒有請求時，它關門并停在當前樓層。15電梯系統(tǒng)的需求電梯系統(tǒng)的需求n使用一個擴展的有窮狀態(tài)機對本產(chǎn)品使用一個擴展的有窮狀態(tài)機對本產(chǎn)品進行規(guī)格說明進行規(guī)格說明:n這個問題中有兩個按鈕集。這個問題中有兩個按鈕集。un部電梯中的每一部都有部電梯中的每一部都有m個按鈕，一個按個按鈕，一個按鈕對應一個樓層。因為這鈕對應一個樓層。因為這mn個按鈕都在個按鈕都在電梯中，所以稱它們?yōu)殡娞葜?，所?/p>

9、稱它們?yōu)殡娞莅粹o電梯按鈕。u每層樓有兩個按鈕，一個請求向上，另一每層樓有兩個按鈕，一個請求向上，另一個請求向下，這些按鈕稱為個請求向下，這些按鈕稱為樓層按鈕樓層按鈕。16電梯系統(tǒng)的需求電梯系統(tǒng)的需求電梯按鈕的狀態(tài)轉換圖如圖電梯按鈕的狀態(tài)轉換圖如圖4.2所示。令所示。令EB(e,f)表示表示按下電梯按下電梯e內的按鈕并請求到內的按鈕并請求到f層去。層去。EB(e,f)有兩個有兩個狀態(tài)，分別是按鈕發(fā)光狀態(tài)，分別是按鈕發(fā)光(打開打開)和不發(fā)光和不發(fā)光(關閉關閉)。更精。更精確地說，確地說，狀態(tài)狀態(tài)是：是：如果電梯按鈕如果電梯按鈕(e,f)發(fā)光且電梯到達發(fā)光且電梯到達f層，該按鈕將熄層，該按鈕將熄滅。

10、相反如果按鈕熄滅，則按下它時，按鈕將發(fā)光。滅。相反如果按鈕熄滅，則按下它時，按鈕將發(fā)光。上述描述中包含了上述描述中包含了兩個事件兩個事件，它們分別是：，它們分別是：17電梯按鈕的狀態(tài)轉換圖電梯按鈕的狀態(tài)轉換圖18電梯按鈕的規(guī)則描述電梯按鈕的規(guī)則描述n定義一個謂詞定義一個謂詞V(e,f)，它的含義如下：，它的含義如下：V(e,f)：電梯：電梯e停在停在f層層u該狀態(tài)轉換規(guī)則的形式化描述如下：該狀態(tài)轉換規(guī)則的形式化描述如下：EBOFF(e,f)+EBP(e,f)+not V(e,f) EBON(e,f)u該轉換規(guī)則可以形式化地表示為：該轉換規(guī)則可以形式化地表示為：EBON(e,f)+EAF(e,f

11、) EBOFF(e,f)19樓層按鈕的狀態(tài)描述樓層按鈕的狀態(tài)描述n令樓層按鈕令樓層按鈕FB(d,f)表示表示f層請求電梯層請求電梯向向d方向運動的按鈕方向運動的按鈕如下：如下：FBON(d,f)：樓層按鈕：樓層按鈕(d,f)打開打開FBOFF(d,f)：樓層按鈕：樓層按鈕(d,f)關閉關閉20樓層按鈕的規(guī)則描述樓層按鈕的規(guī)則描述n如果樓層按鈕已經(jīng)打開，而且一部電如果樓層按鈕已經(jīng)打開，而且一部電梯到達梯到達f層，則按鈕關閉。反之，如果樓層，則按鈕關閉。反之，如果樓層按鈕原來是關閉的，被按下后該按鈕層按鈕原來是關閉的，被按下后該按鈕將打開。將打開。n該規(guī)則包含了以下該規(guī)則包含了以下：u FBP(d

12、,f)：樓層按鈕：樓層按鈕(d,f)被按下被按下uEAF(1n,f)：電梯：電梯1或或或或n到達到達f層層其中其中1n表示或為表示或為1或為或為2或為或為n。21樓層按鈕狀態(tài)轉換圖樓層按鈕狀態(tài)轉換圖22樓層按鈕的規(guī)則描述樓層按鈕的規(guī)則描述n 定義一個謂詞（是一個狀態(tài)）：定義一個謂詞（是一個狀態(tài)）：謂詞謂詞S(d,e,f)：電梯：電梯e停在停在f層并且移動方向由層并且移動方向由d確定為確定為向上向上(d=U)或向下或向下(d=D)或待定或待定(d=N)。n 使用謂詞使用謂詞S(d,e,f)，形式化轉換規(guī)則為：，形式化轉換規(guī)則為：FBOFF(d,f)+FBP(d,f)+not S(d,1n,f)

13、FBON(d,f)FBON(d,f)+EAF(1n,f)+S(d,1n,f) FBOFF(d,f)其中，其中，d=UorD23樓層按鈕的規(guī)則描述樓層按鈕的規(guī)則描述n如果在如果在f層請求電梯向層請求電梯向d方向運動的樓層按鈕處于關閉方向運動的樓層按鈕處于關閉狀態(tài)，現(xiàn)在該按鈕被按下，并且當時沒有正停在狀態(tài)，現(xiàn)在該按鈕被按下，并且當時沒有正停在f層準備層準備向向d方向移動的電梯，則該樓層按鈕打開。反之，如果樓方向移動的電梯，則該樓層按鈕打開。反之，如果樓層按鈕已經(jīng)打開，且至少有一部電梯到達層按鈕已經(jīng)打開，且至少有一部電梯到達f層，該部電梯層，該部電梯將朝將朝d方向運動，則按鈕將關閉。方向運動，則按鈕

14、將關閉。n電梯按鈕狀態(tài)轉換規(guī)則時定義的謂詞電梯按鈕狀態(tài)轉換規(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)24電梯的狀態(tài)電梯的狀態(tài)n定義電梯的定義電梯的3個狀態(tài)：個狀態(tài)：M(d,e,f)：電梯：電梯e正沿正沿d方向移動，即將到達的是第方向移動，即將到達的是第f層層S(d,e,f)：電梯：電梯e停在停在f層，將朝層，將朝d方向移動方向移動(尚未關門尚未關門)W(e,f)：電梯：電梯e在在f層等待層等待(已關門已關門)n3個可觸發(fā)狀態(tài)發(fā)生改變的事件：個可觸發(fā)狀態(tài)發(fā)生改變的事件：DC(e

15、,f)：電梯：電梯e在樓層在樓層f關上門關上門ST(e,f)：電梯：電梯e靠近靠近f層時觸發(fā)傳感器，電梯控制器決定在層時觸發(fā)傳感器，電梯控制器決定在當前樓層電梯是否停下當前樓層電梯是否停下RL：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)，登錄需求：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)，登錄需求25電梯的狀態(tài)轉換圖電梯的狀態(tài)轉換圖圖圖4.4 電梯的狀態(tài)轉換圖電梯的狀態(tài)轉換圖26電梯系統(tǒng)的需求電梯系統(tǒng)的需求n電梯的狀態(tài)轉換規(guī)則電梯的狀態(tài)轉換規(guī)則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ī)

16、則表明，如果電梯第一條規(guī)則表明，如果電梯e停在停在f層準備向上層準備向上移動，且門已經(jīng)關閉，則電梯將向上一樓層移移動，且門已經(jīng)關閉，則電梯將向上一樓層移動。第二條和第三條規(guī)則，分別對應于電梯即動。第二條和第三條規(guī)則，分別對應于電梯即將下降或者沒有待處理的請求的情況。將下降或者沒有待處理的請求的情況。274.2.3 評價評價n規(guī)格說明描述格式簡單：規(guī)格說明描述格式簡單：當前狀態(tài)當前狀態(tài)+事件事件+謂詞謂詞 下個狀態(tài)下個狀態(tài)n易于書寫、驗證，易于轉變成設計或代碼易于書寫、驗證，易于轉變成設計或代碼n維護可以通過修改規(guī)格說明來實現(xiàn)維護可以通過修改規(guī)格說明來實現(xiàn)n比數(shù)據(jù)流圖技術更精確比數(shù)據(jù)流圖技術更精

17、確n三元組三元組(即狀態(tài)、事件、謂詞即狀態(tài)、事件、謂詞)的數(shù)量隨規(guī)模的數(shù)量隨規(guī)模迅速增長迅速增長n沒有處理定時需求沒有處理定時需求284.3 Petri網(wǎng)網(wǎng)n用于確定并發(fā)系統(tǒng)中隱含的定時問題用于確定并發(fā)系統(tǒng)中隱含的定時問題nPetri網(wǎng)包含網(wǎng)包含4種元素，四元組種元素，四元組C=(P,T,I,O) u一組位置一組位置PP1，P2，P3，P4u一組轉換一組轉換Tt1，t2u輸入函數(shù)輸入函數(shù)I：I(t1)=P2，P4、I(t2)=P2u輸出函數(shù)輸出函數(shù)O：O(t1)=P1、O(t2)=P3，P329Petri網(wǎng)的權標網(wǎng)的權標n在在Petri網(wǎng)中權標網(wǎng)中權標(token)的分配的分配n權標可以用向量

18、權標可以用向量(1，2，0，1)表示表示n當每個輸入位置所當每個輸入位置所擁有的權標數(shù)大于等于從擁有的權標數(shù)大于等于從該位置到轉換的線數(shù)該位置到轉換的線數(shù)時，就允許轉換時，就允許轉換nPetri網(wǎng)中權標總數(shù)網(wǎng)中權標總數(shù)不是固定不是固定的的n帶有標記的帶有標記的Petri網(wǎng)成為一個五元組網(wǎng)成為一個五元組(P，T，I，O，M)30Petri網(wǎng)的轉換網(wǎng)的轉換3132333435含禁止線的含禁止線的Petri網(wǎng)網(wǎng)n禁止線是用一個小圓圈而不是用箭頭標記的輸禁止線是用一個小圓圈而不是用箭頭標記的輸入線。入線。n通常，當每個輸入線上至少有一個權標，而禁通常，當每個輸入線上至少有一個權標，而禁止線上沒有權標的

19、時候，相應的轉換才是允許止線上沒有權標的時候，相應的轉換才是允許的。的。36Petri網(wǎng)表示的電梯系統(tǒng)規(guī)格說明網(wǎng)表示的電梯系統(tǒng)規(guī)格說明n每個樓層用一個位置每個樓層用一個位置Ff代表代表(1fm)n電梯用一個權標代表電梯用一個權標代表n在位置在位置Ff上有權標，表示在樓層上有權標，表示在樓層f上有電梯上有電梯1. 電梯按鈕電梯按鈕的行為的行為n第一條約束第一條約束C1：每部電梯有：每部電梯有m個按鈕，每層對應個按鈕，每層對應一個按鈕。當按下一個按鈕時該按鈕指示燈亮，指一個按鈕。當按下一個按鈕時該按鈕指示燈亮，指示電梯移往相應的樓層。當電梯到達指定的樓層時，示電梯移往相應的樓層。當電梯到達指定的樓層時，按鈕將熄滅。按鈕將熄滅。37Petri網(wǎng)表示的網(wǎng)表示的電梯按鈕電梯按鈕n用位置用位置EBf表示樓層表示樓層f的電梯按鈕的電梯按鈕 (1fm)n若電梯內樓層若電梯內樓層f的按鈕被按下，則在的按鈕被按下，則在EBf上有一個權標上有一個權標n電梯按鈕只有在第一次被按下時才會由電梯按鈕只有在第一次被按下時才會由暗變亮，以后再按它則只會被忽略。暗變亮，以后再按它則只會被忽略。38Petri網(wǎng)表示的網(wǎng)表示的電梯按鈕電梯按鈕n假設電梯由假設電梯由g層駛向層駛向f層，位置層，位置Fg上有一個權標上有一個權標n由于每條輸入線上各有一個權標