《形式化說(shuō)明技術(shù)》PPT課件.ppt

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

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

3、有更好的可重用性。,有窮狀態(tài)機(jī),例子：保險(xiǎn)箱的復(fù)合鎖，鎖有三個(gè)位置，分別標(biāo)記為1，2，3，轉(zhuǎn)盤(pán)可向左（L）或向右（R）轉(zhuǎn)動(dòng)。 任意時(shí)刻的6種可能的運(yùn)動(dòng)：1R,1L,2R,2L,3R,3L 假設(shè)組合密碼為：1L,3R,2L，除了這個(gè)次序的任意轉(zhuǎn)動(dòng)都將導(dǎo)致報(bào)警。,保險(xiǎn)箱 鎖定,A,B,保險(xiǎn)箱 解鎖,報(bào)警,1L,轉(zhuǎn)盤(pán)的 任何其 他移動(dòng),3R,2L,轉(zhuǎn)盤(pán)的 任何其 他移動(dòng),轉(zhuǎn)盤(pán)的 任何其 他移動(dòng),初始態(tài),終態(tài),終態(tài),狀態(tài)集J：保險(xiǎn)箱鎖定，A，B，保險(xiǎn)箱解鎖，報(bào)警。 輸入集：1L，1R，2L，2R，3L，3R 轉(zhuǎn)換函數(shù)：T 初始態(tài)S：保險(xiǎn)箱鎖定。 終態(tài)集：保險(xiǎn)箱解鎖，報(bào)警,一個(gè)有窮狀態(tài)機(jī)可以表示為一個(gè)5

4、元組J，K，T，S，F(xiàn) J是一個(gè)有窮的非空狀態(tài)集 K是一個(gè)有窮的非空輸入集 T是一個(gè)從（J-F）*K到J的轉(zhuǎn)換函數(shù) SJ，是一個(gè)初始狀態(tài) F J，是終態(tài)集 例如：菜單 一個(gè)菜單的顯示和一個(gè)狀態(tài)相對(duì)應(yīng) 鍵盤(pán)輸入或鼠標(biāo)點(diǎn)擊對(duì)應(yīng)于一個(gè)事件 當(dāng)前狀態(tài)菜單+事件所選擇的項(xiàng)+謂詞=下個(gè)狀態(tài),電梯的例子,電梯的約束條件： C1：每部電梯有m個(gè)按鈕，每個(gè)按鈕代表一個(gè)樓層。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，同時(shí)電梯駛向相應(yīng)的樓層，到達(dá)按鈕指定的樓層時(shí)指示燈滅。 C2：除了樓的最低層和最高層外，每層樓有兩個(gè)按鈕分別指示是上樓還是下樓。這兩個(gè)按鈕之一被按下時(shí)相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時(shí)燈熄滅，電梯向要求的方向移

5、動(dòng)。 C3：當(dāng)對(duì)電梯沒(méi)有請(qǐng)求時(shí)，它關(guān)門(mén)并停在當(dāng)前樓層。,電梯按鈕,EB（e,f） ：表示按下電梯e內(nèi)的按鈕并請(qǐng)求到f層去 EBP（e,f）:電梯按鈕(e,f)被按下 EAF（e,f）:電梯e到達(dá)f層 謂詞：V(e,f):電梯停在f層 如果電梯按鈕(e,f)處于關(guān)閉狀態(tài)當(dāng)前狀態(tài)，而且電梯(e,f)被按下事件，而且電梯e不在f層謂詞，則該電梯按鈕打開(kāi)發(fā)光下個(gè)狀態(tài)。狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下： EBOFF(e,f)+EBP(e,f)+not V(e,f)=EBON(e,f) EBON(e,f)+EAF(e,f)=EBOFF(e,f),EBOFF(e,f),EBON(e,f),EBP(e,f),EA

6、F(e,f),樓層按鈕,FB(d,f)表示f層請(qǐng)求電梯向d方向運(yùn)動(dòng)的按鈕 FBON(d,f):樓層按鈕(d,f)打開(kāi) FBOFF(d,f)：樓層按鈕(d,f)關(guān)閉 FBP(d,f):樓層按鈕(d,f)被按下 EAF(1n,f):電梯1或或n到達(dá)f層 S(d,e,f)：電梯e停在f層并且移動(dòng)方向由d確定為向上(d=U)或向下(d=D)或待定(d=N) 狀態(tài)轉(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),FBOFF(d,f),FBON(d,f),FBP(d,f),E

7、AF(1n,f),V(e,f)=S(U,e,f) or S(D,e,f) or S(N,e,f) 電梯的三個(gè)狀態(tài)： M(d,e,f)：電梯e正沿d方向移動(dòng)，即將到達(dá)的是第f層 S(d,e,f)：電梯e停在f層，將朝d方向移動(dòng)(尚未關(guān)門(mén)) W(e,f):電梯e在f層等待(已關(guān)門(mén)) 可觸發(fā)狀態(tài)發(fā)生改變的事件 DC(e,f):電梯e在樓層f關(guān)上門(mén) ST(e,f):電梯e靠近f層時(shí)觸發(fā)傳感器，電梯控制器決定在當(dāng)前樓層電梯是否停下 RL：電梯按鈕或樓層按鈕被按下進(jìn)入打開(kāi)狀態(tài)，登錄需求 電梯的狀態(tài)轉(zhuǎn)換規(guī)則 S(U,e,f)+DC(e,f)=M(U,e,f+1) S(D,e,f)+DC(e,f)=M(D,e

8、,f-1) S(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),RL,RL,ST(e,f),RL,RL,RL,DC(e,f),DC(e,f),ST(e,f),Petri網(wǎng),Petri網(wǎng)是用于形式化說(shuō)明定時(shí)問(wèn)題的一種技術(shù) 一組位置 P 為 P1 ， P2 ， P3 ， P4 ，在圖中用圓圈代表位置。 一組轉(zhuǎn)換 T 為 t1 ， t2 ，在圖中用短直線表示轉(zhuǎn)換。 兩個(gè)用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭表示，它們是： I(t1)= P

9、2 ， P4 I(t2)= P2 兩個(gè)用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭表示，它們是: O(t1)= P1 O(t2)= P3 ， P3 ,Petri網(wǎng)包含4種元素：一組位置P、一組轉(zhuǎn)換T、輸入函數(shù)I以及輸出函數(shù)O。 Petri網(wǎng)結(jié)構(gòu)，是一個(gè)四元組C=(P,T,I,O) P=P1,Pn是一個(gè)有窮位置集 T=t1,tm是一個(gè)有窮轉(zhuǎn)換集 I：T-P 為輸入函數(shù)，是由轉(zhuǎn)換到位置組的映射 O： T-P 為輸出函數(shù)，是由轉(zhuǎn)換到位置組的映射,標(biāo)記：(1,2,0,1),標(biāo)記：(2,1,0,0),標(biāo)記：(2,0,2,0),權(quán)標(biāo),Petri網(wǎng)的標(biāo)記M，是由一組位置P到一組非負(fù)整數(shù)的映射： M：P-0,1

10、,2 所以，Petri網(wǎng)成為一個(gè)五元組（P,T,I,O,M）,對(duì)Petri網(wǎng)的擴(kuò)充：加入禁止線。禁止線是用一個(gè)圓圈而不是用箭頭標(biāo)記的輸入線。 通常。當(dāng)每個(gè)輸入線上至少有一個(gè)權(quán)標(biāo)，而禁止線上沒(méi)有權(quán)標(biāo)的時(shí)候，相應(yīng)的轉(zhuǎn) 換才是允許的。,C1:每部電梯有m個(gè)按鈕，每層對(duì)應(yīng)一個(gè)按鈕。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，指示電梯移往相應(yīng)的樓層。當(dāng)電梯到達(dá)指定的樓層時(shí)，按鈕熄滅。 電梯中樓層f的按鈕，在Petri網(wǎng)中用位置EBf表示。(1fm)。在EBf上有一個(gè)權(quán)標(biāo)，表示電梯內(nèi)樓層f的按鈕被按下了。,Fg,電梯按鈕只有在第一次被按下時(shí)才會(huì)由暗變亮，以后再按它會(huì)被忽略。 假設(shè)按鈕沒(méi)有亮，在位置Ebf上沒(méi)有權(quán)標(biāo)，那

11、么在存在禁止線的情況下，轉(zhuǎn)換“EBf”是允許發(fā)生的。按下按鈕之后，則轉(zhuǎn)換被激發(fā)并在EBf上放置了一個(gè)權(quán)標(biāo)，以后無(wú)論再按下多少次按鈕，禁止線與現(xiàn)有權(quán)標(biāo)的組合都決定了轉(zhuǎn)換“EBf被按下”不能再被激發(fā)了，因此，位置EBf上的權(quán)標(biāo)數(shù)不會(huì)多于1,圖4.11 Petri網(wǎng)表示樓層按鈕,4 Z語(yǔ)言簡(jiǎn)介,用Z語(yǔ)言描述的、最簡(jiǎn)單的形式化規(guī)格說(shuō)明含有下述4個(gè)部分： 給定的集合、數(shù)據(jù)類型及常數(shù)。 狀態(tài)定義。 初始狀態(tài)。 操作。,1. 給定的集合 一個(gè)Z規(guī)格說(shuō)明從一系列給定的初始化集合開(kāi)始。所謂初始化集合就是不需要詳細(xì)定義的集合，這種集合用帶方括號(hào)的形式表示。對(duì)于電梯問(wèn)題，給定的初始化集合稱為Button，即所有按鈕

12、的集合，因此，Z規(guī)格說(shuō)明開(kāi)始于：Button 2. 狀態(tài)定義 一個(gè)Z規(guī)格說(shuō)明由若干個(gè)“格(schema)”組成，每個(gè)格含有一組變量說(shuō)明和一系列限定變量取值范圍的謂詞。例如，Z格S的格式如圖4.12所示。,在電梯問(wèn)題中，Button有4個(gè)子集， floor_buttons(樓層按鈕的集合) elevator_buttons(電梯按鈕的集合) buttons(電梯問(wèn)題中所有按鈕的集合) pushed(所有被按的按鈕的集合，即所有處于打開(kāi)狀態(tài)的按鈕的集合)。,3. 初始狀態(tài) 抽象的初始狀態(tài)是指系統(tǒng)第一次開(kāi)啟時(shí)的狀態(tài)。對(duì)于電梯問(wèn)題來(lái)說(shuō)，抽象的初始狀態(tài)為： Button_Init Button_Stat

13、epushed= 上式表示，當(dāng)系統(tǒng)首次開(kāi)啟時(shí)pushed集為空，即所有按鈕都處于關(guān)閉狀態(tài)。 4. 操作 如果一個(gè)原來(lái)處于關(guān)閉狀態(tài)的按鈕被按下，則該按鈕開(kāi)啟，這個(gè)按鈕就被添加到pushed集中。,Button_State button?: button,(button? buttons) (button? pushed) (pushed= pushedbutton?) (button? pushed) (pushed= pushed),Button_State button?: button,(button? buttons) (button? pushed) (pushed= pushedbu

14、tton?) (button? pushed) (pushed= pushed),Push_button,Floor_Arrival,Z 語(yǔ)言實(shí)例：停車場(chǎng)管理系統(tǒng),基本數(shù)據(jù)類型定義 “停車提示”是一個(gè)基本數(shù)據(jù)類型的名字 “停好”和“停車場(chǎng)滿”是該類型的數(shù)據(jù)可能的取值 停車提示= 停好| 停車場(chǎng)滿 全局變量聲明 在Z 語(yǔ)言中，N 和Z 屬于基本數(shù)據(jù)集合，分別表示正整數(shù)集合和整數(shù)集合。 停車場(chǎng)容量: Z/*變量聲明*/ 停車場(chǎng)容量0/*變量約束*/,狀態(tài)定義 每個(gè)系統(tǒng)有唯一的狀態(tài)定義，可以為狀態(tài)命名。本例中為系統(tǒng)狀態(tài)命名為“停車場(chǎng)狀態(tài)”。狀態(tài)定義中首先聲明一或多個(gè)表示系統(tǒng)狀態(tài)的變量，這里的變量名為

15、“停車數(shù)量”，類型為整數(shù)。該變量的約束條件為取值大于等于0，小于等于最大停車數(shù)量。 停車場(chǎng)狀態(tài) 停車數(shù)量: Z/*狀態(tài)變量聲明*/ 停車數(shù)量0 停車數(shù)量停車場(chǎng)容量,初始化 定義系統(tǒng)狀態(tài)變量的初始值。系統(tǒng)的初始化定義是唯一的。,操作定義 每個(gè)系統(tǒng)可以定義若干個(gè)操作。 Z 語(yǔ)言中操作的定義是基于狀態(tài)的，而不是基于過(guò)程的。 該操作如何改變了系統(tǒng)的狀態(tài)變量的值？ 該操作有哪些輸入變量？ 有哪些輸出變量？ 當(dāng)一個(gè)操作改變了某個(gè)系統(tǒng)狀態(tài)變量x時(shí)，在操作定義的第一行寫(xiě)出狀態(tài)變化聲明x。 當(dāng)一個(gè)操作未改變?nèi)魏蜗到y(tǒng)狀態(tài)變量時(shí)，即可以在操作定義第一行寫(xiě)出以下?tīng)顟B(tài)聲明狀態(tài)變量（可省略）。,操作定義（續(xù)）,操作定義也

16、可以采用以下形式 進(jìn)入停車場(chǎng)正常停車停車場(chǎng)滿 表示： 操作“進(jìn)入停車場(chǎng)”分為“正常停車”和“停車場(chǎng)滿”兩種可能情況，具體執(zhí)行時(shí)選擇哪種情況，由環(huán)境滿足哪種操作的約束條件來(lái)決定。,評(píng)價(jià),Z語(yǔ)言優(yōu)勢(shì)： (1) 可以比較容易地發(fā)現(xiàn)用Z寫(xiě)的規(guī)格說(shuō)明的錯(cuò)誤，特別是在自己審查規(guī)格說(shuō)明，及根據(jù)形式化的規(guī)格說(shuō)明來(lái)審查設(shè)計(jì)與代碼時(shí)，情況更是如此。 (2) 用Z寫(xiě)規(guī)格說(shuō)明時(shí)，要求作者十分精確地使用Z說(shuō)明符。由于對(duì)精確性的要求很高，從而和非形式化規(guī)格說(shuō)明相比，減少了模糊性、不一致性和遺漏。 (3) Z是一種形式化語(yǔ)言，在需要時(shí)開(kāi)發(fā)者可以嚴(yán)格地驗(yàn)證規(guī)格說(shuō)明的正確性。 (4) 雖然完全學(xué)會(huì)Z語(yǔ)言相當(dāng)困難，但是，經(jīng)驗(yàn)表明，只學(xué)過(guò)中學(xué)數(shù)學(xué)的軟件開(kāi)發(fā)人員仍然可以只用比較短的時(shí)間就學(xué)會(huì)編寫(xiě)Z規(guī)