軟件工程第4章(不講)

單擊此處編輯母版標(biāo)題樣式,單擊此處編輯母版文本樣式,第二級(jí),第三級(jí),第四級(jí),第五級(jí),*,*,*,第,4,章 形式化說(shuō)明技術(shù),4.1,概述,4.2,有窮狀態(tài)機(jī),4.3 Petri,網(wǎng),4.4 Z,語(yǔ)言,4.5,小結(jié),1,形式化方法,是描述系統(tǒng)性質(zhì)的基于,數(shù)學(xué),的技術(shù)，有堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)。,按照形式化的程度，劃分成非形式化、半形式化和形式化,3,類。,用自然語(yǔ)言描述需求規(guī)格說(shuō)明，是典型的非形式化方法。,用數(shù)據(jù)流圖或?qū)嶓w,-,聯(lián)系圖建立模型，是典型的半形式化方法。,2,4.1.1,非形式化方法的缺點(diǎn),自然語(yǔ)言書(shū)寫的規(guī)格說(shuō)明書(shū)，可能存在,矛盾,二義性,含糊性,不完整性,抽象層次混亂,3,4.1.2,形式化方法的優(yōu)點(diǎn),簡(jiǎn)潔準(zhǔn)確,，是理想的建模工具,驗(yàn)證需求，以,發(fā)現(xiàn)存在的矛盾和不完整性,平滑過(guò)渡，也可以用于設(shè)計(jì),提供了高層,確認(rèn),的手段,證明設(shè)計(jì)符合規(guī)格說(shuō)明,證明程序代碼正確地實(shí)現(xiàn)了設(shè)計(jì)結(jié)果,4,4.1.3,應(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ā)方法。,(6),應(yīng)該建立詳盡的文檔。,(7),不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)。,(8),不應(yīng)該盲目依賴形式化方法。,(9),應(yīng)該測(cè)試、測(cè)試再測(cè)試。,(10),應(yīng)該重用。,5,4.2,有窮狀態(tài)機(jī),例如,當(dāng)有多個(gè)申請(qǐng)占用,CPU,運(yùn)行的進(jìn)程時(shí),有關(guān),CPU,分配的進(jìn)程的狀態(tài)遷移。,6,進(jìn)程的狀態(tài)遷移,7,保險(xiǎn)箱的狀態(tài)轉(zhuǎn)換圖,例：一個(gè)保險(xiǎn)箱上裝了一個(gè)復(fù)合鎖，鎖有三個(gè)位置，分別標(biāo)記為,1,、,2,、,3,，轉(zhuǎn)盤可向左,(L),或向右,(R),轉(zhuǎn)動(dòng)。這樣，在任意時(shí)刻轉(zhuǎn)盤都有,6,種可能的運(yùn)動(dòng)，即,1L,、,1R,、,2L,、,2R,、,3L,和,3R,。保險(xiǎn)箱的組合密碼是,1L,、,3R,、,2L,，轉(zhuǎn)盤的任何其他運(yùn)動(dòng)都將引起報(bào)警。,8,保險(xiǎn)箱的狀態(tài)轉(zhuǎn)換圖,9,有窮狀態(tài)機(jī)的狀態(tài)轉(zhuǎn)換表,10,有窮狀態(tài)機(jī)的表示,包括,5,個(gè)部分：,狀態(tài)集,J,、,輸入集,K,、由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個(gè)狀態(tài),(,次態(tài),),的,轉(zhuǎn)換函數(shù),T,、,初始態(tài),S,和,終態(tài)集,F,。,保險(xiǎn)箱的有窮狀態(tài)機(jī)：,狀態(tài)集,J,：保險(xiǎn)箱鎖定，,A,，,B,，保險(xiǎn)箱解鎖，報(bào)警。,輸入集,K,：,1L,，,1R,，,2L,，,2R,，,3L,，,3R,。,轉(zhuǎn)換函數(shù),T,：如表,4.1,所示。,初始態(tài),S,：保險(xiǎn)箱鎖定。,終態(tài)集,F,：保險(xiǎn)箱解鎖，報(bào)警。,11,有窮狀態(tài)機(jī)5元組表示,表示為一個(gè),5,元組,(J,，,K,，,T,，,S,，,F),，其中：,J,是一個(gè)有窮的非空狀態(tài)集；,K,是一個(gè)有窮的非空輸入集；,T,是一個(gè)從,(J-F)K,到,J,的轉(zhuǎn)換函數(shù)；,SJ,，是一個(gè)初始狀態(tài)；,FJ,，是終態(tài)集。,12,狀態(tài)轉(zhuǎn)換表示形式,狀態(tài)的每個(gè)轉(zhuǎn)換都具有下面的形式：,當(dāng)前狀態(tài),菜單,+,事件,所選擇的項(xiàng),下個(gè)狀態(tài)。,加入,謂詞集,P,把有窮狀態(tài)機(jī)擴(kuò)展為一個(gè),6,元組，其中每個(gè)謂詞都是系統(tǒng)全局狀態(tài),Y,的函數(shù)。轉(zhuǎn)換函數(shù),T,則是一個(gè)從,(J-F)KP,到,J,的函數(shù)。轉(zhuǎn)換規(guī)則形式如下：,當(dāng)前狀態(tài),菜單,+,事件,所選擇的項(xiàng),+,謂詞,下個(gè)狀態(tài)。,13,電梯系統(tǒng)的需求,自然語(yǔ)言描述的對(duì)電梯系統(tǒng)的需求：,在一幢,m,層的大廈中需要一套控制,n,部電梯的產(chǎn)品，要求這,n,部電梯按照約束條件,C1,，,C2,和,C3,在樓層間移動(dòng)。,C1,：每部電梯內(nèi)有,m,個(gè)按鈕，每個(gè)按鈕代表一個(gè)樓層。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，同時(shí)電梯駛向相應(yīng)的樓層，到達(dá)按鈕指定的樓層時(shí)指示燈熄滅。,C2,：除了大廈的最低層和最高層之外，每層樓都有兩個(gè)按鈕分別請(qǐng)求電梯上行和下行。這兩個(gè)按鈕之一被按下時(shí)相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時(shí)燈熄滅，電梯向要求的方向移動(dòng)。,C3,：當(dāng)對(duì)電梯沒(méi)有請(qǐng)求時(shí)，它關(guān)門并停在當(dāng)前樓層。,14,電梯系統(tǒng)的需求,使用一個(gè)擴(kuò)展的有窮狀態(tài)機(jī)對(duì)本產(chǎn)品進(jìn)行規(guī)格說(shuō)明,:,這個(gè)問(wèn)題中有兩個(gè)按鈕集。,n,部電梯中的每一部都有,m,個(gè)按鈕，一個(gè)按鈕對(duì)應(yīng)一個(gè)樓層。因?yàn)檫@,mn,個(gè)按鈕都在電梯中，所以稱它們?yōu)?電梯按鈕,。,每層樓有兩個(gè)按鈕，一個(gè)請(qǐng)求向上，另一個(gè)請(qǐng)求向下，這些按鈕稱為,樓層按鈕,。,15,電梯系統(tǒng)的需求,電梯按鈕的狀態(tài)轉(zhuǎn)換圖如圖,4.2,所示。令,EB(e,f),表示按下電梯,e,內(nèi)的按鈕并請(qǐng)求到,f,層去。,EB(e,f),有兩個(gè)狀態(tài)，分別是按鈕發(fā)光,(,打開(kāi),),和不發(fā)光,(,關(guān)閉,),。更精確地說(shuō)，,狀態(tài),是：,EBON(e,f),：電梯按鈕,(e,f),打開(kāi),EBOFF(e,f),：電梯按鈕,(e,f),關(guān)閉,如果電梯按鈕,(e,f),發(fā)光且電梯到達(dá),f,層，該按鈕將熄滅。相反如果按鈕熄滅，則按下它時(shí)，按鈕將發(fā)光。上述描述中包含了,兩個(gè)事件,，它們分別是：,EBP(e,f),：電梯按鈕,(e,f),被按下,EAF(e,f),：電梯,e,到達(dá),f,層,16,電梯按鈕的狀態(tài)轉(zhuǎn)換圖,17,電梯按鈕的規(guī)則描述,定義一個(gè)謂詞,V(e,f),，它的含義如下：,V(e,f),：電梯,e,停在,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),反之，如果電梯到達(dá),f,層，而且電梯按鈕是打開(kāi)的，于是它就會(huì)熄滅。,該轉(zhuǎn)換規(guī)則可以形式化地表示為：,EBON(e,f)+EAF(e,f)EBOFF(e,f),18,樓層按鈕的狀態(tài)描述,令樓層按鈕,FB(d,f),表示,f,層請(qǐng)求電梯向,d,方向運(yùn)動(dòng)的按鈕,樓層按鈕的狀態(tài),如下：,FBON(d,f),：樓層按鈕,(d,f),打開(kāi),FBOFF(d,f),：樓層按鈕,(d,f),關(guān)閉,19,樓層按鈕的規(guī)則描述,如果樓層按鈕已經(jīng)打開(kāi)，而且一部電梯到達(dá),f,層，則按鈕關(guān)閉。反之，如果樓層按鈕原來(lái)是關(guān)閉的，被按下后該按鈕將打開(kāi)。,該規(guī)則包含了以下,兩個(gè)事件,：,FBP(d,f),：樓層按鈕,(d,f),被按下,EAF(1n,f),：電梯,1,或,或,n,到達(dá),f,層,其中,1n,表示或?yàn)?1,或?yàn)?2,或?yàn)?n,。,20,樓層按鈕狀態(tài)轉(zhuǎn)換圖,21,樓層按鈕的規(guī)則描述,定義一個(gè)謂詞（是一個(gè)狀態(tài)）：,謂詞,S(d,e,f),：電梯,e,停在,f,層并且移動(dòng)方向由,d,確定為向上,(d=U),或向下,(d=D),或待定,(d=N),。,使用謂詞,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=UorD,22,樓層按鈕的規(guī)則描述,如果在,f,層請(qǐng)求電梯向,d,方向運(yùn)動(dòng)的樓層按鈕處于關(guān)閉狀態(tài)，現(xiàn)在該按鈕被按下，并且當(dāng)時(shí)沒(méi)有正停在,f,層準(zhǔn)備向,d,方向移動(dòng)的電梯，則該樓層按鈕打開(kāi)。反之，如果樓層按鈕已經(jīng)打開(kāi)，且至少有一部電梯到達(dá),f,層，該部電梯將朝,d,方向運(yùn)動(dòng)，則按鈕將關(guān)閉。,電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時(shí)定義的謂詞,V(e,f),，可以用謂詞,S(d,e,f),重新定義：,V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f),23,電梯的狀態(tài),定義電梯的,3,個(gè)狀態(tài)：,M(d,e,f),：電梯,e,正沿,d,方向移動(dòng)，即將到達(dá)的是第,f,層,S(d,e,f),：電梯,e,停在,f,層，將朝,d,方向移動(dòng),(,尚未關(guān)門,),W(e,f),：電梯,e,在,f,層等待,(,已關(guān)門,),3,個(gè)可觸發(fā)狀態(tài)發(fā)生改變的事件：,DC(e,f),：電梯,e,在樓層,f,關(guān)上門,ST(e,f),：電梯,e,靠近,f,層時(shí)觸發(fā)傳感器，電梯控制器決定在當(dāng)前樓層電梯是否停下,RL,：電梯按鈕或樓層按鈕被按下進(jìn)入打開(kāi)狀態(tài)，登錄需求,24,電梯的狀態(tài)轉(zhuǎn)換圖,圖,4.4,電梯的狀態(tài)轉(zhuǎn)換圖,25,電梯系統(tǒng)的需求,電梯的狀態(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,f-1),S(N,e,f)+DC(e,f)W(e,f),第一條規(guī)則表明，如果電梯,e,停在,f,層準(zhǔn)備向上移動(dòng)，且門已經(jīng)關(guān)閉，則電梯將向上一樓層移動(dòng)。第二條和第三條規(guī)則，分別對(duì)應(yīng)于電梯即將下降或者沒(méi)有待處理的請(qǐng)求的情況。,26,4.2.3,評(píng)價(jià),規(guī)格說(shuō)明描述格式簡(jiǎn)單：,當(dāng)前狀態(tài),+,事件,+,謂詞 下個(gè)狀態(tài),易于書(shū)寫、驗(yàn)證，易于轉(zhuǎn)變成設(shè)計(jì)或代碼,維護(hù)可以通過(guò)修改規(guī)格說(shuō)明來(lái)實(shí)現(xiàn),比數(shù)據(jù)流圖技術(shù)更精確,三元組,(,即狀態(tài)、事件、謂詞,),的數(shù)量隨規(guī)模迅速增長(zhǎng),沒(méi)有處理定時(shí)需求,27,4.3 Petri,網(wǎng),用于確定并發(fā)系統(tǒng)中隱含的定時(shí)問(wèn)題,Petri,網(wǎng)包含,4,種元素，四元組,C=(P,T,I,O),一組位置,P,P1,，,P2,，,P3,，,P4,一組轉(zhuǎn)換,T,t1,，,t2,輸入函數(shù),I,：,I(t1)=,P2,，,P4,、,I(t2)=,P2,輸出函數(shù),O,：,O(t1)=,P1,、,O(t2)=,P3,，,P3,28,Petri網(wǎng)的權(quán)標(biāo),在,Petri,網(wǎng)中權(quán)標(biāo),(token),的分配,權(quán)標(biāo)可以用向量,(1,，,2,，,0,，,1),表示,當(dāng)每個(gè)輸入位置所,擁有的權(quán)標(biāo)數(shù)大于等于從該位置到轉(zhuǎn)換的線數(shù),時(shí)，就允許轉(zhuǎn)換,Petri,網(wǎng)中權(quán)標(biāo)總數(shù),不是固定,的,帶有標(biāo)記的,Petri,網(wǎng)成為一個(gè)五元組,(P,，,T,，,I,，,O,，,M),29,Petri,網(wǎng)的轉(zhuǎn)換,30,31,32,處理兩個(gè)進(jìn)程的同步問(wèn)題,33,34,含禁止線的Petri網(wǎng),禁止線是用一個(gè)小圓圈而不是用箭頭標(biāo)記的輸入線。,通常，當(dāng)每個(gè)輸入線上至少有一個(gè)權(quán)標(biāo)，而禁止線上沒(méi)有權(quán)標(biāo)的時(shí)候，相應(yīng)的轉(zhuǎn)換才是允許的。,35,Petri,網(wǎng)表示的電梯系統(tǒng)規(guī)格說(shuō)明,每個(gè)樓層用一個(gè)位置,F,f,代表,(1fm),電梯用一個(gè)權(quán)標(biāo)代表,在位置,F,f,上有權(quán)標(biāo)，表示在樓層,f,上有電梯,1.,電梯按鈕,的行為,第一條約束,C1,：每部電梯有,m,個(gè)按鈕，每層對(duì)應(yīng)一個(gè)按鈕。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，指示電梯移往相應(yīng)的樓層。當(dāng)電梯到達(dá)指定的樓層時(shí)，按鈕將熄滅。,36,Petri,網(wǎng)表示的,電梯按鈕,用位置,EB,f,表示樓層,f,的電梯按鈕,(1fm),若電梯內(nèi)樓層,f,的按鈕被按下，則在,EB,f,上有一個(gè)權(quán)標(biāo),電梯按鈕只有在第一次被按下時(shí)才會(huì)由暗變亮，以后再按它則只會(huì)被忽略。,37,Petri,網(wǎng)表示的,電梯按鈕,假設(shè)電梯由,g,層駛向,f,層，位置,F,g,上有一個(gè)權(quán)標(biāo),由于每條輸入線上各有一個(gè)權(quán)標(biāo)，轉(zhuǎn)換“電梯在運(yùn)行”被激發(fā)，從而,EB,f,和,F,g,上的權(quán)標(biāo)被移走，按鈕,EB,f,被關(guān)閉，在位置,F,f,上出現(xiàn)一個(gè)新權(quán)標(biāo)，即轉(zhuǎn)換的激發(fā)使電梯由,g,層駛到,f,層。,38,Petri,網(wǎng)表示的,樓層按鈕,2.,樓層按鈕,的行為,第二條約束,C2,：除了第一層與頂層之外，每個(gè)樓層都有兩個(gè)按鈕，一個(gè)要求電梯上行，另一個(gè)要求電梯下行。這些按鈕在按下時(shí)發(fā)亮，當(dāng)電梯到達(dá)該層并將向指定方向移動(dòng)時(shí)，相應(yīng)的按鈕才會(huì)熄滅。,用位置,FB,f,u,和,FB,f,d,表示樓層按鈕，分別代表,f,樓層請(qǐng)求電梯上行和下行的按鈕。,底層的按鈕為,FB,1,u,，最高層的按鈕為,FB,m,d,，中間每一層有兩個(gè)按鈕,FB,f,u,和,FB,f,d,(1,f,m),。,39,Petri網(wǎng)表示樓層按鈕,電梯由,g,層駛向,f,層,如果兩個(gè)按鈕都亮了，則只有一個(gè)按鈕熄滅,第三條約束,C3,：當(dāng)電梯沒(méi)有收到請(qǐng)求時(shí)，它將停留在當(dāng)前樓層并關(guān)門。,(FBf,u,和,FBf,d,上無(wú)權(quán)標(biāo)）,40,