《軟件工程第4章(不講)》由會員分享，可在線閱讀，更多相關(guān)《軟件工程第4章(不講)（40頁珍藏版）》請在裝配圖網(wǎng)上搜索。

1、單擊此處編輯母版標(biāo)題樣式,單擊此處編輯母版文本樣式,第二級,第三級,第四級,第五級,*,*,*,第,4,章 形式化說明技術(shù),4.1,概述,4.2,有窮狀態(tài)機,4.3 Petri,網(wǎng),4.4 Z,語言,4.5,小結(jié),1,形式化方法,是描述系統(tǒng)性質(zhì)的基于,數(shù)學(xué),的技術(shù)，有堅實的數(shù)學(xué)基礎(chǔ)。,按照形式化的程度，劃分成非形式化、半形式化和形式化,3,類。,用自然語言描述需求規(guī)格說明，是典型的非形式化方法。,用數(shù)據(jù)流圖或?qū)嶓w,-,聯(lián)系圖建立模型，是典型的半形式化方法。,2,4.1.1,非形式化方法的缺點,自然語言書寫的規(guī)格說明書，可能存在,矛盾,二義性,含糊性,不完整性,抽象層次混亂,3,4.1.2,形式

2、化方法的優(yōu)點,簡潔準(zhǔn)確,，是理想的建模工具,驗證需求，以,發(fā)現(xiàn)存在的矛盾和不完整性,平滑過渡，也可以用于設(shè)計,提供了高層,確認(rèn),的手段,證明設(shè)計符合規(guī)格說明,證明程序代碼正確地實現(xiàn)了設(shè)計結(jié)果,4,4.1.3,應(yīng)用形式化方法的準(zhǔn)則,(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)該重用。,5,4.2,有窮狀態(tài)機,例如,當(dāng)有多個申請

3、占用,CPU,運行的進程時,有關(guān),CPU,分配的進程的狀態(tài)遷移。,6,進程的狀態(tài)遷移,7,保險箱的狀態(tài)轉(zhuǎn)換圖,例：一個保險箱上裝了一個復(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)盤的任何其他運動都將引起報警。,8,保險箱的狀態(tài)轉(zhuǎn)換圖,9,有窮狀態(tài)機的狀態(tài)轉(zhuǎn)換表,10,有窮狀態(tài)機的表示,包括,5,個部分：,狀態(tài)集,J,、,輸入集,K,、由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個狀態(tài),(,次態(tài),),的,

4、轉(zhuǎn)換函數(shù),T,、,初始態(tài),S,和,終態(tài)集,F,。,保險箱的有窮狀態(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,：保險箱解鎖，報警。,11,有窮狀態(tài)機5元組表示,表示為一個,5,元組,(J,，,K,，,T,，,S,，,F),，其中：,J,是一個有窮的非空狀態(tài)集；,K,是一個有窮的非空輸入集；,T,是一個從,(J-F)K,到,J,的轉(zhuǎn)換函數(shù)；,SJ,，是一個初始狀態(tài)；,FJ,，是終態(tài)集。,12,狀態(tài)轉(zhuǎn)換表示形式,狀態(tài)的每個

5、轉(zhuǎn)換都具有下面的形式：,當(dāng)前狀態(tài),菜單,+,事件,所選擇的項,下個狀態(tài)。,加入,謂詞集,P,把有窮狀態(tài)機擴展為一個,6,元組，其中每個謂詞都是系統(tǒng)全局狀態(tài),Y,的函數(shù)。轉(zhuǎn)換函數(shù),T,則是一個從,(J-F)KP,到,J,的函數(shù)。轉(zhuǎn)換規(guī)則形式如下：,當(dāng)前狀態(tài),菜單,+,事件,所選擇的項,+,謂詞,下個狀態(tài)。,13,電梯系統(tǒng)的需求,自然語言描述的對電梯系統(tǒng)的需求：,在一幢,m,層的大廈中需要一套控制,n,部電梯的產(chǎn)品，要求這,n,部電梯按照約束條件,C1,，,C2,和,C3,在樓層間移動。,C1,：每部電梯內(nèi)有,m,個按鈕，每個按鈕代表一個樓層。當(dāng)按下一個按鈕時該按鈕指示燈亮，同時電梯駛向相應(yīng)的樓層

6、，到達(dá)按鈕指定的樓層時指示燈熄滅。,C2,：除了大廈的最低層和最高層之外，每層樓都有兩個按鈕分別請求電梯上行和下行。這兩個按鈕之一被按下時相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時燈熄滅，電梯向要求的方向移動。,C3,：當(dāng)對電梯沒有請求時，它關(guān)門并停在當(dāng)前樓層。,14,電梯系統(tǒng)的需求,使用一個擴展的有窮狀態(tài)機對本產(chǎn)品進行規(guī)格說明,:,這個問題中有兩個按鈕集。,n,部電梯中的每一部都有,m,個按鈕，一個按鈕對應(yīng)一個樓層。因為這,mn,個按鈕都在電梯中，所以稱它們?yōu)?電梯按鈕,。,每層樓有兩個按鈕，一個請求向上，另一個請求向下，這些按鈕稱為,樓層按鈕,。,15,電梯系統(tǒng)的需求,電梯按鈕的狀態(tài)轉(zhuǎn)換圖如圖,4

7、.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,f),被按下,EAF(e,f),：電梯,e,到達(dá),f,層,16,電梯按鈕的狀態(tài)轉(zhuǎn)換圖,17,電梯按鈕的規(guī)則描述,定義一個謂

8、詞,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)EBOFF(e,f),18,樓層按鈕的狀態(tài)描述,令樓層按鈕,FB(d,f),表示,f,層請求電梯向,d,方向

9、運動的按鈕,樓層按鈕的狀態(tài),如下：,FBON(d,f),：樓層按鈕,(d,f),打開,FBOFF(d,f),：樓層按鈕,(d,f),關(guān)閉,19,樓層按鈕的規(guī)則描述,如果樓層按鈕已經(jīng)打開，而且一部電梯到達(dá),f,層，則按鈕關(guān)閉。反之，如果樓層按鈕原來是關(guān)閉的，被按下后該按鈕將打開。,該規(guī)則包含了以下,兩個事件,：,FBP(d,f),：樓層按鈕,(d,f),被按下,EAF(1n,f),：電梯,1,或,或,n,到達(dá),f,層,其中,1n,表示或為,1,或為,2,或為,n,。,20,樓層按鈕狀態(tài)轉(zhuǎn)換圖,21,樓層按鈕的規(guī)則描述,定義一個謂詞（是一個狀態(tài)）：,謂詞,S(d,e,f),：電梯,e,停在,f,層

10、并且移動方向由,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,層請求電梯向,d,方向運動的樓層按鈕處于關(guān)閉狀態(tài)，現(xiàn)在該按鈕被按下，并且當(dāng)時沒有正停在,f,層準(zhǔn)備向,d,方向移動的電梯，則該樓層按鈕打開。反之，如果樓層按鈕已經(jīng)打開，且至少有一部電梯到達(dá),f,層，該部電梯將朝,d,方向運動，則按鈕將關(guān)

11、閉。,電梯按鈕狀態(tài)轉(zhuǎn)換規(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),23,電梯的狀態(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)門,),3,個可觸發(fā)狀態(tài)發(fā)生改變的事件：,DC(e,f),：電梯,e,在樓層,f,關(guān)上門,ST(e,f),：電梯,e,靠近,f,層時觸發(fā)傳感器，電梯控制器決定在當(dāng)前樓層電梯是否

12、停下,RL,：電梯按鈕或樓層按鈕被按下進入打開狀態(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)備向上移動，且門已經(jīng)關(guān)閉，則電梯將向上一樓層移動。第二條和第三條規(guī)則，分別對應(yīng)于電梯即將下降或者沒有待處理的請求的情況。,26,4.2.3,評價,規(guī)格說明描述格式簡單：,當(dāng)前狀態(tài),+,事件,+,謂詞 下個狀態(tài),易于書寫、驗證，易于轉(zhuǎn)變成設(shè)計或代

13、碼,維護可以通過修改規(guī)格說明來實現(xiàn),比數(shù)據(jù)流圖技術(shù)更精確,三元組,(,即狀態(tài)、事件、謂詞,),的數(shù)量隨規(guī)模迅速增長,沒有處理定時需求,27,4.3 Petri,網(wǎng),用于確定并發(fā)系統(tǒng)中隱含的定時問題,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,

14、，,1),表示,當(dāng)每個輸入位置所,擁有的權(quán)標(biāo)數(shù)大于等于從該位置到轉(zhuǎn)換的線數(shù),時，就允許轉(zhuǎn)換,Petri,網(wǎng)中權(quán)標(biāo)總數(shù),不是固定,的,帶有標(biāo)記的,Petri,網(wǎng)成為一個五元組,(P,，,T,，,I,，,O,，,M),29,Petri,網(wǎng)的轉(zhuǎn)換,30,31,32,處理兩個進程的同步問題,33,34,含禁止線的Petri網(wǎng),禁止線是用一個小圓圈而不是用箭頭標(biāo)記的輸入線。,通常，當(dāng)每個輸入線上至少有一個權(quán)標(biāo)，而禁止線上沒有權(quán)標(biāo)的時候，相應(yīng)的轉(zhuǎn)換才是允許的。,35,Petri,網(wǎng)表示的電梯系統(tǒng)規(guī)格說明,每個樓層用一個位置,F,f,代表,(1fm),電梯用一個權(quán)標(biāo)代表,在位置,F,f,上有權(quán)標(biāo)，表示在樓層

15、,f,上有電梯,1.,電梯按鈕,的行為,第一條約束,C1,：每部電梯有,m,個按鈕，每層對應(yīng)一個按鈕。當(dāng)按下一個按鈕時該按鈕指示燈亮，指示電梯移往相應(yīng)的樓層。當(dāng)電梯到達(dá)指定的樓層時，按鈕將熄滅。,36,Petri,網(wǎng)表示的,電梯按鈕,用位置,EB,f,表示樓層,f,的電梯按鈕,(1fm),若電梯內(nèi)樓層,f,的按鈕被按下，則在,EB,f,上有一個權(quán)標(biāo),電梯按鈕只有在第一次被按下時才會由暗變亮，以后再按它則只會被忽略。,37,Petri,網(wǎng)表示的,電梯按鈕,假設(shè)電梯由,g,層駛向,f,層，位置,F,g,上有一個權(quán)標(biāo),由于每條輸入線上各有一個權(quán)標(biāo)，轉(zhuǎn)換“電梯在運行”被激發(fā)，從而,EB,f,和,F,g

16、,上的權(quán)標(biāo)被移走，按鈕,EB,f,被關(guān)閉，在位置,F,f,上出現(xiàn)一個新權(quán)標(biāo)，即轉(zhuǎn)換的激發(fā)使電梯由,g,層駛到,f,層。,38,Petri,網(wǎng)表示的,樓層按鈕,2.,樓層按鈕,的行為,第二條約束,C2,：除了第一層與頂層之外，每個樓層都有兩個按鈕，一個要求電梯上行，另一個要求電梯下行。這些按鈕在按下時發(fā)亮，當(dāng)電梯到達(dá)該層并將向指定方向移動時，相應(yīng)的按鈕才會熄滅。,用位置,FB,f,u,和,FB,f,d,表示樓層按鈕，分別代表,f,樓層請求電梯上行和下行的按鈕。,底層的按鈕為,FB,1,u,，最高層的按鈕為,FB,m,d,，中間每一層有兩個按鈕,FB,f,u,和,FB,f,d,(1,f,m),。,39,Petri網(wǎng)表示樓層按鈕,電梯由,g,層駛向,f,層,如果兩個按鈕都亮了，則只有一個按鈕熄滅,第三條約束,C3,：當(dāng)電梯沒有收到請求時，它將停留在當(dāng)前樓層并關(guān)門。,(FBf,u,和,FBf,d,上無權(quán)標(biāo)）,40,