第7講形式化說明技術(shù)ppt課件

1、第4章形式化說明技術(shù)什么是形式化說明技術(shù)l從廣義上講，形式化方法是指將離散數(shù)學的方法用于解決軟件工程領(lǐng)域的問題，主要包括建立精確的數(shù)學模型以及對模型的分析活動。l狹義的講，形式化方法是運用形式化語言，進行形式化的規(guī)格描述、模型推理和驗證的方法。l就形式化建模而言，形式化表示必須包含一組定義其語法語義的形式化規(guī)則。這些規(guī)則可用于分析給定的表達式是否符合語法規(guī)定，或證明該表達式具有某種性質(zhì)。形式化說明技術(shù)l用自然語言描述需求規(guī)格說明，是典型的非形式化方法。用數(shù)據(jù)流圖或ER圖建立模型，是典型的半形式化方法。所謂形式化方法，就是基于數(shù)學的技術(shù)來描述系統(tǒng)的性質(zhì)的方法。l非形式化方法的缺點l形式化方法的優(yōu)

2、點應(yīng)用形式化方法的準則(1) 應(yīng)該選用適當?shù)谋硎痉椒ā?2) 應(yīng)該形式化，但不要過分形式化。(3) 應(yīng)該估算成本。(4) 應(yīng)該有形式化方法顧問隨時提供咨詢。 (5) 不應(yīng)該放棄傳統(tǒng)的開發(fā)方法。把形式化方法和結(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋硎强赡艿?，而且由?取長補短往往能獲得很好的效果。 (6) 應(yīng)該建立詳盡的文檔。建議使用自然語言注釋形式化的規(guī)格說明書，以幫助用戶和維護人員理解系統(tǒng)。 (9) 應(yīng)該測試、測試再測試。 (10) 應(yīng)該重用。即使采用了形式化方法，軟件重用仍然是降低軟件成本和提高軟件質(zhì)量的惟一合理的方法。而且用形式化方法說明的軟件構(gòu)件具有清晰定義的功能和接口，使得它們有更好的可重用

3、性。 有窮狀態(tài)機l例子：保險箱的復合鎖，鎖有三個位置，分別標記為1，2，3，轉(zhuǎn)盤可向左L或向右R轉(zhuǎn)動。l任意時刻的6種可能的運動：1R,1L,2R,2L,3R,3Ll假設(shè)組合密碼為：1L,3R,2L，除了這個次序的任意轉(zhuǎn)動都將導致報警。保險箱鎖定AB保險箱解鎖報警1L轉(zhuǎn)盤的任何其他移動3R2L轉(zhuǎn)盤的任何其他移動轉(zhuǎn)盤的任何其他移動初始態(tài)終態(tài)終態(tài) 當前狀態(tài) 次態(tài) 轉(zhuǎn)盤動作 保險箱鎖定AB1LA報警報警1R報警報警報警2L報警報警保險箱解鎖2R報警報警報警3L報警報警報警3R報警B報警狀態(tài)集狀態(tài)集J：保險箱鎖定，保險箱鎖定，A，B，保險箱解鎖，報警，保險箱解鎖，報警。輸入集：輸入集：1L，1R，2L

4、，2R，3L，3R轉(zhuǎn)換函數(shù)：轉(zhuǎn)換函數(shù)：T初始態(tài)初始態(tài)S：保險箱鎖定。：保險箱鎖定。終態(tài)集：終態(tài)集：保險箱解鎖，報警保險箱解鎖，報警l一個有窮狀態(tài)機可以表示為一個5元組J，K，T，S，F(xiàn)lJ是一個有窮的非空狀態(tài)集lK是一個有窮的非空輸入集lT是一個從J-F）*K到J的轉(zhuǎn)換函數(shù)lSJ，是一個初始狀態(tài)lF J，是終態(tài)集l例如：菜單l一個菜單的顯示和一個狀態(tài)相對應(yīng)l鍵盤輸入或鼠標點擊對應(yīng)于一個事件l當前狀態(tài)菜單+事件所選擇的項+謂詞=下個狀態(tài)電梯的例子l電梯的約束條件：lC1：每部電梯有m個按鈕，每個按鈕代表一個樓層。當按下一個按鈕時該按鈕指示燈亮，同時電梯駛向相應(yīng)的樓層，到達按鈕指定的樓層時指示燈滅

5、。lC2：除了樓的最低層和最高層外，每層樓有兩個按鈕分別指示是上樓還是下樓。這兩個按鈕之一被按下時相應(yīng)的指示燈亮，當電梯到達此樓層時燈熄滅，電梯向要求的方向移動。lC3：當對電梯沒有請求時，它關(guān)門并停在當前樓層。電梯按鈕lEBe,f） ：表示按下電梯e內(nèi)的按鈕并請求到f層去lEBPe,f）:電梯按鈕(e,f)被按下lEAFe,f）:電梯e到達f層l謂詞：V(e,f):電梯停在f層l如果電梯按鈕(e,f)處于關(guān)閉狀態(tài)當前狀態(tài)，而且電梯(e,f)被按下事件，而且電梯e不在f層謂詞，則該電梯按鈕打開發(fā)光下個狀態(tài)。狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下：lEBOFF(e,f)+EBP(e,f)+not V(e,

6、f)=EBON(e,f)lEBON(e,f)+EAF(e,f)=EBOFF(e,f)EBOFF(e,f)EBON(e,f)EBP(e,f)EAF(e,f)樓層按鈕lFB(d,f)表示f層請求電梯向d方向運動的按鈕lFBON(d,f):樓層按鈕(d,f)翻開 FBOFF(d,f)：樓層按鈕(d,f)關(guān)閉lFBP(d,f):樓層按鈕(d,f)被按下 EAF(1n,f):電梯1或或n到達f層lS(d,e,f)：電梯e停在f層并且移動方向由d確定為向上(d=U)或向下(d=D)或待定(d=N)l狀態(tài)轉(zhuǎn)換規(guī)則：lFBOFF(d,f)+FBP(d,f)+not S(d,1n,f)=FBON(d,f)lFB

7、ON(d,f)+EAF(1n,f)+S(d,1n,f)=FBOFF(d,f)FBOFF(d,f)FBON(d,f)FBP(d,f)EAF(1n,f)lV(e,f)=S(U,e,f) or S(D,e,f) or S(N,e,f)l電梯的三個狀態(tài)：lM(d,e,f)：電梯e正沿d方向移動，即將到達的是第f層lS(d,e,f)：電梯e停在f層，將朝d方向移動(尚未關(guān)門)lW(e,f):電梯e在f層等待(已關(guān)門)l可觸發(fā)狀態(tài)發(fā)生改變的事件lDC(e,f):電梯e在樓層f關(guān)上門lST(e,f):電梯e靠近f層時觸發(fā)傳感器，電梯控制器決定在當前樓層電梯是否停下lRL：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)

8、，登錄需求l電梯的狀態(tài)轉(zhuǎn)換規(guī)則lS(U,e,f)+DC(e,f)=M(U,e,f+1)lS(D,e,f)+DC(e,f)=M(D,e,f-1)lS(N,e,f)+DC(e,f)=W(e,f)S(U,e,f)S(N,e,f)M(U,e,f+1)S(D,e,f)M(D,e,f)M(U,e,f)M(D,e,f-1)W(e,f)DC(e,f)RLRLST(e,f)RLRLRLDC(e,f)DC(e,f)ST(e,f)Petri網(wǎng)lPetri網(wǎng)是用于形式化說明定時問題的一種技術(shù)l一組位置 P 為 P1 ， P2 ， P3 ， P4 ，在圖中用圓圈代表位置。 l一組轉(zhuǎn)換 T 為 t1 ， t2 ，在圖中用

9、短直線表示轉(zhuǎn)換。 l兩個用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭表示，它們是： lI(t1)= P2 ， P4 I(t2)= P2 l兩個用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭表示，它們是: lO(t1)= P1 O(t2)= P3 ， P3 p1p2p4t2t1p3lPetri網(wǎng)包含4種元素：一組位置P、一組轉(zhuǎn)換T、輸入函數(shù)I以及輸出函數(shù)O。lPetri網(wǎng)結(jié)構(gòu)，是一個四元組C=(P,T,I,O)lP=P1,Pn是一個有窮位置集lT=t1,tm是一個有窮轉(zhuǎn)換集l I：T-P 為輸入函數(shù)，是由轉(zhuǎn)換到位置組的映射lO： T-P 為輸出函數(shù)，是由轉(zhuǎn)換到位置組的映射p1p2p4t2t1p3p1p

10、2p4t2t1p3標志：(1,2,0,1)標志：(2,1,0,0)標志：(2,0,2,0)p1p2p4t2t1p3權(quán)標權(quán)標lPetri網(wǎng)的標記M，是由一組位置P到一組非負整數(shù)的映射：lM：P-0,1,2l所以，Petri網(wǎng)成為一個五元組P,T,I,O,M）p1p2p3t1對Petri網(wǎng)的擴充：加入禁止線。禁止線是用一個圓圈而不是用箭頭標記的輸入線。通常。當每個輸入線上至少有一個權(quán)標，而禁止線上沒有權(quán)標的時候，相應(yīng)的轉(zhuǎn)換才是允許的。lC1:每部電梯有m個按鈕，每層對應(yīng)一個按鈕。當按下一個按鈕時該按鈕指示燈亮，指示電梯移往相應(yīng)的樓層。當電梯到達指定的樓層時，按鈕熄滅。l電梯中樓層f的按鈕，在Pet

11、ri網(wǎng)中用位置EBf表示。(1fm)。在EBf上有一個權(quán)標，表示電梯內(nèi)樓層f的按鈕被按下了。FgFfEBfEBf被按下電梯在運行電梯在運行電梯按鈕只有在第一次被按下時才會由暗變亮，以后電梯按鈕只有在第一次被按下時才會由暗變亮，以后再按它會被忽略。再按它會被忽略。 假設(shè)按鈕沒有亮，在位置假設(shè)按鈕沒有亮，在位置Ebf上沒有權(quán)標，那么上沒有權(quán)標，那么在存在禁止線的情況下，轉(zhuǎn)換在存在禁止線的情況下，轉(zhuǎn)換“EBf是允許發(fā)生的。是允許發(fā)生的。按下按鈕之后，則轉(zhuǎn)換被激發(fā)并在按下按鈕之后，則轉(zhuǎn)換被激發(fā)并在EBf上放置了一個權(quán)上放置了一個權(quán)標，以后無論再按下多少次按鈕，禁止線與現(xiàn)有權(quán)標標，以后無論再按下多少次按

12、鈕，禁止線與現(xiàn)有權(quán)標的組合都決定了轉(zhuǎn)換的組合都決定了轉(zhuǎn)換“EBf被按下不能再被激發(fā)了，被按下不能再被激發(fā)了，因而，位置因而，位置EBf上的權(quán)標數(shù)不會多于上的權(quán)標數(shù)不會多于1圖4.11 Petri網(wǎng)表示樓層按鈕4 Z語言簡介語言簡介用用Z Z語言描述的、最簡單的形式化規(guī)格說明含有下述語言描述的、最簡單的形式化規(guī)格說明含有下述4 4個部個部分：分：給定的集合、數(shù)據(jù)類型及常數(shù)。給定的集合、數(shù)據(jù)類型及常數(shù)。狀態(tài)定義。狀態(tài)定義。初始狀態(tài)。初始狀態(tài)。操作。操作。l1. 1. 給定的集合給定的集合l一個一個Z Z規(guī)格說明從一系列給定的初始化集合開始。所謂初始化集合就規(guī)格說明從一系列給定的初始化集合開始。所謂

13、初始化集合就是不需要詳細定義的集合，這種集合用帶方括號的形式表示。對于電是不需要詳細定義的集合，這種集合用帶方括號的形式表示。對于電梯問題，給定的初始化集合稱為梯問題，給定的初始化集合稱為ButtonButton，即所有按鈕的集合，因而，即所有按鈕的集合，因而，Z Z規(guī)格說明開始于：規(guī)格說明開始于：ButtonButtonl2. 2. 狀態(tài)定義狀態(tài)定義l一個一個Z Z規(guī)格說明由若干個規(guī)格說明由若干個“格格(schema)”(schema)”組成，每個格含有一組變量組成，每個格含有一組變量說明和一系列限定變量取值范圍的謂詞。例如，說明和一系列限定變量取值范圍的謂詞。例如，Z Z格格S S的格式如

14、圖的格式如圖4.124.12所示。所示。在電梯問題中，在電梯問題中，ButtonButton有有4 4個子集，個子集，floor_buttons(floor_buttons(樓層按鈕的集合樓層按鈕的集合) )elevator_buttons(elevator_buttons(電梯按鈕的集合電梯按鈕的集合) )buttons(buttons(電梯問題中所有按鈕的集合電梯問題中所有按鈕的集合) )pushed(pushed(所有被按的按鈕的集合，即所有處于打開狀態(tài)的按鈕的集合所有被按的按鈕的集合，即所有處于打開狀態(tài)的按鈕的集合) )。3. 初始狀態(tài)抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。對于電梯

15、問題來說，抽象的初始狀態(tài)為：Button_Init Button_Statepushed=上式表示，當系統(tǒng)首次開啟時pushed集為空，即所有按鈕都處于關(guān)閉狀態(tài)。4. 操作如果一個原來處于關(guān)閉狀態(tài)的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到pushed集中。 Button_Statebutton?: button(button? buttons)(button? pushed) (pushed= pushedbutton?) (button? pushed) (pushed= pushed)Button_Statebutton?: button(button? buttons)(button

16、? pushed) (pushed= pushedbutton?) (button? pushed) (pushed= pushed)Push_buttonFloor_ArrivalZ 語言實例：停車場管理系統(tǒng)語言實例：停車場管理系統(tǒng)l基本數(shù)據(jù)類型定義l“停車提示是一個基本數(shù)據(jù)類型的名字l“停好和“停車場滿是該類型的數(shù)據(jù)可能的取值l停車提示= 停好| 停車場滿l全局變量聲明l在Z 語言中，N 和Z 屬于基本數(shù)據(jù)集合，分別表示正整數(shù)集合和整數(shù)集合。l停車場容量: Z/*變量聲明*/l停車場容量0/*變量約束*/l狀態(tài)定義l每個系統(tǒng)有唯一的狀態(tài)定義，可以為狀態(tài)命名。本例中為系統(tǒng)狀態(tài)命名為“停車場狀

17、態(tài)”。狀態(tài)定義中首先聲明一或多個表示系統(tǒng)狀態(tài)的變量，這里的變量名為“停車數(shù)量”，類型為整數(shù)。該變量的約束條件為取值大于等于0，小于等于最大停車數(shù)量。l停車場狀態(tài)l停車數(shù)量: Z/*狀態(tài)變量聲明*/l停車數(shù)量0l停車數(shù)量停車場容量l初始化l定義系統(tǒng)狀態(tài)變量的初始值。系統(tǒng)的初始化定義是唯一的。l操作定義l每個系統(tǒng)可以定義若干個操作。lZ 語言中操作的定義是基于狀態(tài)的，而不是基于過程的。l該操作如何改變了系統(tǒng)的狀態(tài)變量的值？l該操作有哪些輸入變量？l有哪些輸出變量？l當一個操作改變了某個系統(tǒng)狀態(tài)變量x時，在操作定義的第一行寫出狀態(tài)變化聲明x。l當一個操作未改變?nèi)魏蜗到y(tǒng)狀態(tài)變量時，即可以在操作定義第一

18、行寫出以下狀態(tài)聲明狀態(tài)變量可省略）。l操作定義續(xù)）l操作定義也可以采用以下形式l進入停車場 正常停車停車場滿l表示：l操作“進入停車場分為“正常停車和“停車場滿兩種可能情況，具體執(zhí)行時選擇哪種情況，由環(huán)境滿足哪種操作的約束條件來決定。評價Z Z語言優(yōu)勢：語言優(yōu)勢：(1) (1) 可以比較容易地發(fā)現(xiàn)用可以比較容易地發(fā)現(xiàn)用Z Z寫的規(guī)格說明的錯誤，特別是在自己審寫的規(guī)格說明的錯誤，特別是在自己審查規(guī)格說明，及根據(jù)形式化的規(guī)格說明來審查設(shè)計與代碼時，情況更查規(guī)格說明，及根據(jù)形式化的規(guī)格說明來審查設(shè)計與代碼時，情況更是如此。是如此。(2) (2) 用用Z Z寫規(guī)格說明時，要求作者十分精確地使用寫規(guī)格說明時，要求作者十分精確地使用Z Z說明符。由于對精說明符。由于對精確性的要求很高，從而和非形式化規(guī)格說明相比，減少了模糊性、不確性的要求很高，從而和非形式化規(guī)格說明相比，減少了模糊性、不一致性和遺漏。一致性和遺漏。 (3) Z(3) Z是一種形式化語言，在需要時開發(fā)者可以嚴格地驗證規(guī)格說明是一種形式化語言，在需要時開發(fā)者可以嚴格地驗證規(guī)格說明的正確性。的正確性。(4) (4