第4章軟件工程教學(xué)課件

習(xí)題:1舉例對(duì)比形式化方法和欠形式化方法的優(yōu)缺點(diǎn)。2在什么情況下應(yīng)該使用形式化說(shuō)明技術(shù)?使用形式化說(shuō)明技術(shù)時(shí)應(yīng)遵守哪些準(zhǔn)則?3考慮下述的自動(dòng)化圖書(shū)館流通系統(tǒng)：每本書(shū)都有一個(gè)條形碼，每個(gè)借閱人都有一個(gè)帶有條形碼的卡片。當(dāng)一個(gè)借閱人想借一本書(shū)時(shí)，圖書(shū)管理員掃描書(shū)上的條形碼和借閱人卡片上的條形碼，然后在計(jì)算機(jī)終端上輸入C；當(dāng)歸還一本書(shū)時(shí)，圖書(shū)管理員將再做一次掃描，并輸入R。圖書(shū)管理員可以把一些書(shū)加到(+)圖書(shū)集合中，也可以刪除(-)它們。借閱人可以在終端上查找到某個(gè)作者所有的書(shū)(輸入“A=”和作者名字)，或具有指定標(biāo)題的所有書(shū)籍(輸入“T=”和標(biāo)題)，或?qū)儆谔囟ㄖ黝}范圍內(nèi)的所有圖書(shū)(輸入“S=”加主題范圍)。最后，如果借閱人想借的書(shū)已被別人借走，圖書(shū)管理員將給這本書(shū)設(shè)置一個(gè)預(yù)約，以便書(shū)歸還時(shí)把書(shū)留給預(yù)約的借閱人(輸入“H=”加書(shū)號(hào))。試用有窮狀態(tài)機(jī)說(shuō)明上述的圖書(shū)流通系統(tǒng)。2023/7/231湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄教學(xué)內(nèi)容4.1概述4.2有窮狀態(tài)機(jī)4.3Petri網(wǎng)4.4Z語(yǔ)言4.5小結(jié)2023/7/232湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄第4章形式化說(shuō)明技術(shù)

根據(jù)形式化的程度,可以把軟件工程方法劃分成非形式化、半形式化和形式化三類。使用自然語(yǔ)言描述需求規(guī)格說(shuō)明,是典型的非形式化方法。使用數(shù)據(jù)流圖或?qū)嶓w—關(guān)系圖等圖形符號(hào)建立模型,是典型的半形式化方法。用于開(kāi)發(fā)計(jì)算機(jī)系統(tǒng)的形式化方法,是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù),也就是說(shuō),如果一個(gè)方法有堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ),那么它就是形式化的。2023/7/233湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄4.1概述4.1.1非形式化方法的缺點(diǎn)基本上使用自然語(yǔ)言描述的系統(tǒng)規(guī)格說(shuō)明,可能存在矛盾、二義性、含糊性、不完整性以及抽象層次混雜等問(wèn)題。2023/7/234湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄4.1.2形式化方法的優(yōu)點(diǎn)數(shù)學(xué)最有用的性質(zhì)之一是,它能夠簡(jiǎn)潔、準(zhǔn)確地描述物理現(xiàn)象、對(duì)象或動(dòng)作的結(jié)果,因此是理想的建模工具。在軟件開(kāi)發(fā)過(guò)程中使用數(shù)學(xué)的另一個(gè)優(yōu)點(diǎn)是,可以在軟件工程活動(dòng)之間平滑地過(guò)渡。不僅功能規(guī)格說(shuō)明,而且系統(tǒng)設(shè)計(jì)也可以用數(shù)學(xué)表達(dá),當(dāng)然,程序代碼也是一種數(shù)學(xué)符號(hào)。數(shù)學(xué)作為軟件開(kāi)發(fā)工具的最后一個(gè)優(yōu)點(diǎn)是,它提供了高層確認(rèn)的手段?？梢允褂脭?shù)學(xué)方法證明,設(shè)計(jì)符合規(guī)格說(shuō)明,程序代碼正確地反映了設(shè)計(jì)結(jié)果。2023/7/235湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄4.1.3應(yīng)用形式化方法的準(zhǔn)則

應(yīng)用形式化方法的幾條準(zhǔn)則:選擇適用于當(dāng)前項(xiàng)目的符號(hào)系統(tǒng)。應(yīng)該形式化,但不要過(guò)分形式化。應(yīng)該進(jìn)行成本/效益分析。需要有形式化方法的顧問(wèn)。不要放棄傳統(tǒng)的開(kāi)發(fā)方法。2023/7/236湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄應(yīng)該建立詳盡的文檔。不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)。不應(yīng)該盲目依賴形式化方法。應(yīng)該測(cè)試、測(cè)試再測(cè)試。應(yīng)該重用。2023/7/237湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄4.2有窮狀態(tài)機(jī)

利用有窮狀態(tài)機(jī)可以準(zhǔn)確地描述一個(gè)系統(tǒng),因此是表達(dá)規(guī)格說(shuō)明的一種形式化方法。4.2.1基本概念下面通過(guò)一個(gè)簡(jiǎn)單例子介紹有窮狀態(tài)機(jī)的基本概念。2023/7/238湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

一個(gè)保險(xiǎn)箱上裝了一個(gè)復(fù)合鎖，鎖有三個(gè)位置，分別標(biāo)記為1、2、3，轉(zhuǎn)盤(pán)可向左(L)或向右(R)轉(zhuǎn)動(dòng)。這樣，在任意時(shí)刻轉(zhuǎn)盤(pán)都有6種可能的運(yùn)動(dòng)，即1L、1R、2L、2R、3L和3R。保險(xiǎn)箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤(pán)的任何其他運(yùn)動(dòng)都將引起報(bào)警。圖4.1描繪了保險(xiǎn)箱的狀態(tài)轉(zhuǎn)換情況。圖4.1是一個(gè)有窮狀態(tài)機(jī)的狀態(tài)轉(zhuǎn)換圖。狀態(tài)轉(zhuǎn)換并不一定要用圖形方式描述，表4.1的表格形式也可以表達(dá)同樣的信息。2023/7/239湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.1保險(xiǎn)箱的狀態(tài)轉(zhuǎn)換圖2023/7/2310湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄2023/7/2311湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

從上面這個(gè)簡(jiǎn)單例子可以看出,一個(gè)有窮狀態(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。如果使用更形式化的術(shù)語(yǔ),一個(gè)有窮狀態(tài)機(jī)可以表示為一個(gè)5元組(J,R,T,S,F),其中：

J是一個(gè)有窮的非空狀態(tài)集；

K是一個(gè)有窮的非空輸入集；

T是一個(gè)從(J-F)×K到J的轉(zhuǎn)換函數(shù)；

S∈J,是一個(gè)初始狀態(tài)；

FJ,是終態(tài)集。2023/7/2312湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

當(dāng)前狀態(tài)[菜單]+事件[所選擇的項(xiàng)]下個(gè)狀態(tài)

為了對(duì)一個(gè)系統(tǒng)進(jìn)行規(guī)格說(shuō)明,通常都需要對(duì)有窮狀態(tài)機(jī)做一個(gè)很有用的擴(kuò)展,即在前述的5元組中加入第6個(gè)組件——謂詞集P,即把有窮狀態(tài)機(jī)擴(kuò)展為一個(gè)6元組,其中每個(gè)謂詞都是系統(tǒng)全局狀態(tài)Y的函數(shù)。轉(zhuǎn)換函數(shù)T現(xiàn)在是一個(gè)從(J-F)×K×P到J的函數(shù)?，F(xiàn)在的轉(zhuǎn)換規(guī)則形式如下：

當(dāng)前狀態(tài)[菜單]+事件[所選擇的項(xiàng)]+謂詞下個(gè)狀態(tài)2023/7/2313湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄4.2.2例子(電梯問(wèn)題)

電梯按鈕的狀態(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è)事件,它們分別是：2023/7/2314湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.2電梯按鈕的狀態(tài)轉(zhuǎn)換圖2023/7/2315湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄EBP(e,f)：電梯按鈕(e,f)被按下

EAF(e,f)：電梯e到達(dá)f層為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(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)+notV(e,f)EBON(e,f)

反之,如果電梯到達(dá)f層,而且電梯按鈕是打開(kāi)的,于是它就會(huì)熄滅。這條轉(zhuǎn)換規(guī)則可以形式化地表示為：

EBON(e,f)+EAF(e,f)EBOFF(e,f)2023/7/2316湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

接下來(lái)讓我們考慮樓層按鈕。令FB(d,f)表示f層的按鈕請(qǐng)求電梯向d方向運(yùn)動(dòng),樓層按鈕FB(d,f)的狀態(tài)轉(zhuǎn)換圖如圖4.3所示。樓層按鈕的狀態(tài)如下:FBON(d,f)：樓層按鈕(d,f)打開(kāi)；

FBOFF(d,f)：樓層按鈕(d,f)關(guān)閉。如果樓層按鈕已經(jīng)打開(kāi),而且一部電梯到達(dá)f層,則按鈕關(guān)閉。反之,如果樓層按鈕原來(lái)是關(guān)閉的,被按下后該按鈕將打開(kāi)。這段敘述中包含了以下兩個(gè)事件:FBP(d,f)：樓層按鈕(d,f)被按下

EAF(1··n,f)：電梯1或…或n到達(dá)f層其中1··n表示或?yàn)?或?yàn)?…或?yàn)閚。2023/7/2317湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.3樓層按鈕的狀態(tài)轉(zhuǎn)換圖2023/7/2318湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則,同樣也需要一個(gè)謂詞,它是S(d,e,f),它的定義如下。

S(d,e,f)：電梯e停在f層并且移動(dòng)方向由d確定為向上(d=U)或向下(d=D)或待定(d=N)。這個(gè)謂詞實(shí)際上是一個(gè)狀態(tài),形式化方法允許把事件和狀態(tài)作為謂詞對(duì)待。使用謂詞S(d,e,f),形式化轉(zhuǎn)換規(guī)則為：

FBOFF(d,f)+FBP(d,f)+notS(d,1··n,f)FBON(d,f)

FBON(d,f)+EAF(1··n,f)+S(d,1··n,f)FBOFF(d,f)

其中,d=UorD。2023/7/2319湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

也就是說(shuō),如果在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)orS(D,e,f)orS(N,e,f)2023/7/2320湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

下面定義電梯的三個(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))。其中S(d,e,f)狀態(tài)已在討論樓層按鈕時(shí)定義過(guò),但是,現(xiàn)在的定義更完備一些。圖4.4是電梯的狀態(tài)轉(zhuǎn)換圖。注意,三個(gè)電梯停止?fàn)顟B(tài)S(U,e,f)、S(N,e,f)和S(D,e,f)已被組合成一個(gè)大的狀態(tài),這樣做的目的是減少狀態(tài)總數(shù)以簡(jiǎn)化流圖。2023/7/2321湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.4電梯的狀態(tài)轉(zhuǎn)換圖2023/7/2322湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

圖4.4中包含了下述三個(gè)可觸發(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),登錄需求。2023/7/2323湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

最后,給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則。為簡(jiǎn)單起見(jiàn),這里給出的規(guī)則僅發(fā)生在關(guān)門(mén)之時(shí)。

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),且門(mén)已經(jīng)關(guān)閉,則電梯將向上一樓層移動(dòng)。第二條和第三條規(guī)則,分別對(duì)應(yīng)于電梯即將下降或者沒(méi)有待處理的請(qǐng)求的情況。2023/7/2324湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄4.2.3評(píng)價(jià)有窮狀態(tài)機(jī)方法采用了一種簡(jiǎn)單的格式來(lái)描述規(guī)格說(shuō)明：

當(dāng)前狀態(tài)+事件+謂詞下個(gè)狀態(tài)這種形式的規(guī)格說(shuō)明易于書(shū)寫(xiě)、易于驗(yàn)證,而且可以比較容易地把它轉(zhuǎn)變成設(shè)計(jì)或程序代碼。事實(shí)上,可以開(kāi)發(fā)一個(gè)CASE工具把一個(gè)有窮狀態(tài)機(jī)規(guī)格說(shuō)明直接轉(zhuǎn)變?yōu)樵创a。維護(hù)可以通過(guò)重新轉(zhuǎn)變來(lái)實(shí)現(xiàn),也就是說(shuō),如果需要一個(gè)新的狀態(tài)或事件,首先修改規(guī)格說(shuō)明,然后直接由新的規(guī)格說(shuō)明生成新版本的產(chǎn)品。2023/7/2325湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

有窮狀態(tài)機(jī)方法比數(shù)據(jù)流圖技術(shù)更精確,而且和它一樣易于理解。不過(guò),它也有缺點(diǎn)：在開(kāi)發(fā)一個(gè)大系統(tǒng)時(shí)三元組(即狀態(tài)、事件、謂詞)的數(shù)量會(huì)迅速增長(zhǎng)。此外,和數(shù)據(jù)流圖方法一樣,形式化的有窮狀態(tài)機(jī)方法也沒(méi)有處理定時(shí)需求。下節(jié)將介紹的Petri網(wǎng)技術(shù),是一種可處理定時(shí)問(wèn)題的形式化方法。2023/7/2326湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄4.3Petri網(wǎng)4.3.1基本概念

Petri網(wǎng)包含4種元素：一組位置P、一組轉(zhuǎn)換T、輸入函數(shù)I以及輸出函數(shù)O。圖4.5舉例說(shuō)明了Petri網(wǎng)的組成。其中:

一組位置P為{P1,P2,P3,P4},在圖中用圓圈代表位置。一組轉(zhuǎn)換T為{t1,t2},在圖中用短直線表示轉(zhuǎn)換。2023/7/2327湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.5Petri網(wǎng)的組成2023/7/2328湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

兩個(gè)用于轉(zhuǎn)換的輸入函數(shù),用由位置指向轉(zhuǎn)換的箭頭表示,它們是：

I(t1)={P2,P4}I(t2)={P2}

兩個(gè)用于轉(zhuǎn)換的輸出函數(shù),用由轉(zhuǎn)換指向位置的箭頭表示,它們是：

O(t1)={P1}O(t2)={P3,P3}

注意,輸出函數(shù)O(t2)中有兩個(gè)P3,是因?yàn)橛袃蓚€(gè)箭頭由t2指向P3。2023/7/2329湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

更形式化的Petri網(wǎng)結(jié)構(gòu),是一個(gè)四元組C=(P,T,I,O)。其中:P={P1,……,Pn}是一個(gè)有窮位置集,n≥0。

T={t1,……,tm}是一個(gè)有窮轉(zhuǎn)換集,m≥0,且T和P不相交。

I：T→P∞為輸入函數(shù),是由轉(zhuǎn)換到位置無(wú)序單位組(bags)的映射。

O：T→P∞為輸出函數(shù),是由轉(zhuǎn)換到位置無(wú)序單位組的映射。一個(gè)無(wú)序單位組或多重組是允許一個(gè)元素有多個(gè)實(shí)例的廣義集。2023/7/2330湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄Petri網(wǎng)的標(biāo)記是在Petri網(wǎng)中令牌(token)的分配。例如,在圖4.6中有4個(gè)令牌,其中一個(gè)在P1中,兩個(gè)在P2中,P3中沒(méi)有,還有一個(gè)在P4中。上述標(biāo)記可以用向量(1,2,0,1)表示。由于P2和P4中有令牌,因此t1啟動(dòng)(即被激發(fā))。通常,當(dāng)每個(gè)輸入位置所擁有的令牌數(shù)等于從該位置到轉(zhuǎn)換的線數(shù)時(shí),就允許轉(zhuǎn)換。當(dāng)t1被激發(fā)時(shí),P2和P4上各有一個(gè)令牌被移出,而P1上則增加一個(gè)令牌。Petri網(wǎng)中令牌總數(shù)不是固定的,在這個(gè)例子中兩個(gè)令牌被移出,而P1上只能增加一個(gè)令牌。2023/7/2331湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

在圖4.6中P2上有令牌,因此t2也可以被激發(fā)。當(dāng)t2被激發(fā)時(shí),P2上將移走一個(gè)令牌,而P3上新增加兩個(gè)令牌。Petri網(wǎng)具有非確定性,也就是說(shuō),如果數(shù)個(gè)轉(zhuǎn)換都達(dá)到了激發(fā)條件,則其中任意一個(gè)都可以被激發(fā)。圖4.6所示Petri網(wǎng)的標(biāo)記為(1,2,0,1),t1和t2都可以被激發(fā)。假設(shè)t1被激發(fā)了,則結(jié)果如圖4.7所示,標(biāo)記為(2,1,0,0)。此時(shí),只有t2可以被激發(fā)。如果t2也被激發(fā)了,則令牌從P2中移出,兩個(gè)新令牌被放在P3上,結(jié)果如圖4.8所示,標(biāo)記為(2,0,2,0)。2023/7/2332湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.6帶標(biāo)記的Petri網(wǎng)2023/7/2333湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.7圖4.6的Petri網(wǎng)在轉(zhuǎn)換t1被激發(fā)后的情況2023/7/2334湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.8圖4.7的Petri網(wǎng)在轉(zhuǎn)換t2被激發(fā)后的情況2023/7/2335湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

更形式化地說(shuō),Petri網(wǎng)C=(P,T,I,O)中的標(biāo)記M,是由一組位置P到一組非負(fù)整數(shù)的映射：

M：P→{0,1,2,……}

這樣,帶有標(biāo)記的Petri網(wǎng)成為一個(gè)五元組(P,T,I,O,M)。對(duì)Petri網(wǎng)的一個(gè)重要擴(kuò)充是加入禁止線。如圖4.9所示,禁止線是用一個(gè)小圓圈而不是用箭頭標(biāo)記的輸入線。通常,當(dāng)每個(gè)輸入線上至少有一個(gè)令牌,而禁止線上沒(méi)有令牌的時(shí)候,相應(yīng)的轉(zhuǎn)換才是允許的。在圖14.9中,P3上有一個(gè)令牌而P2上沒(méi)有令牌,因此轉(zhuǎn)換t1可以被激發(fā)。2023/7/2336湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.9含禁止線的Petri網(wǎng)2023/7/2337湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄4.3.2應(yīng)用實(shí)例讓我們把Petri網(wǎng)應(yīng)用于上一節(jié)討論過(guò)的電梯問(wèn)題。當(dāng)用Petri網(wǎng)表示電梯系統(tǒng)的規(guī)格說(shuō)明時(shí),每個(gè)樓層用一個(gè)位置Ff代表(1≤f≤m),在Petri網(wǎng)中電梯是用一個(gè)令牌代表的。在位置Ff上有令牌,表示在樓層f上有電梯。1.電梯按鈕為了用Petri網(wǎng)表達(dá)電梯按鈕的規(guī)格說(shuō)明,在Petri網(wǎng)中還必須設(shè)置其他的位置。電梯中樓層f的按鈕,在Petri網(wǎng)中用位置EBf表示(1≤f≤m)。在EBf上有一個(gè)令牌,就表示電梯內(nèi)樓層f的按鈕被按下了。2023/7/2338湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

電梯按鈕只有在第一次被按下時(shí)才會(huì)由暗變亮,以后再按它則只會(huì)被忽略。圖4.10所示的Petri網(wǎng)準(zhǔn)確地描述了電梯按鈕的行為規(guī)律。首先,假設(shè)按鈕沒(méi)有發(fā)亮,顯然在位置EBf上沒(méi)有令牌,從而在存在禁止線的情況下,轉(zhuǎn)換“EBf被按下”是允許發(fā)生的。假設(shè)現(xiàn)在按下按鈕,則轉(zhuǎn)換被激發(fā)并在EBf上放置了一個(gè)令牌,如圖4.10所示。以后不論再按下多少次按鈕,禁止線與現(xiàn)有令牌的組合都決定了轉(zhuǎn)換“EBf被按下”不能再被激發(fā)了,因此,位置EBf上的令牌數(shù)不會(huì)多于1。2023/7/2339湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.10Petri網(wǎng)表示的電梯按鈕2023/7/2340湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

假設(shè)電梯由g層駛向f層,因?yàn)殡娞菰趃層,如圖4.10所示,位置Fg上有一個(gè)令牌。由于每條輸入線上各有一個(gè)令牌,轉(zhuǎn)換“電梯在運(yùn)行”被激發(fā),從而EBf和Fg上的令牌被移走,按鈕EBf被關(guān)閉,在位置Ff上出現(xiàn)一個(gè)新令牌,即轉(zhuǎn)換的激發(fā)使電梯由g層駛到f層。事實(shí)上,電梯由g層移到f層是需要時(shí)間的,為處理這個(gè)情況及其他類似的問(wèn)題(例如,由于物理上的原因按鈕被按下后不能馬上發(fā)亮),Petri網(wǎng)模型中必須加入時(shí)限。也就是說(shuō),在標(biāo)準(zhǔn)Petri網(wǎng)中轉(zhuǎn)換是瞬時(shí)完成的,而在現(xiàn)實(shí)情況下就需要時(shí)間控制Petri網(wǎng),以使轉(zhuǎn)換與非零時(shí)間相聯(lián)系。2023/7/2341湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄2.樓層按鈕在Petri網(wǎng)中樓層按鈕用位置和表示,分別代表f樓層請(qǐng)求電梯上行和下行的按鈕。底層的按鈕為,最高層的按鈕為,中間每一層有兩個(gè)按鈕和(1＜f＜m)。圖4.11所示的情況為電梯由g層駛向f層。根據(jù)電梯乘客的要求,某一個(gè)樓層按鈕亮或兩個(gè)樓層按鈕都亮。如果兩個(gè)按鈕都亮了,則只有一個(gè)按鈕熄滅。圖4.11所示的Petri網(wǎng)可以保證,當(dāng)兩個(gè)按鈕都亮了的時(shí)候,只有一個(gè)按鈕熄滅。但是要保證按鈕熄滅正確,則需要更復(fù)雜的Petri網(wǎng)模型。2023/7/2342湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.11Petri網(wǎng)表示樓層按鈕2023/7/2343湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

最后,讓我們考慮第三條約束。第三條約束C3：當(dāng)電梯沒(méi)有收到請(qǐng)求時(shí),它將停留在當(dāng)前樓層并關(guān)門(mén)。這條約束很容易實(shí)現(xiàn),如圖4.11所示,當(dāng)沒(méi)有請(qǐng)求(和上無(wú)令牌)時(shí),任何一個(gè)轉(zhuǎn)換“電梯在運(yùn)行”都不能被激發(fā)。2023/7/2344湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄4.4Z語(yǔ)言4.4.1簡(jiǎn)介本節(jié)結(jié)合電梯問(wèn)題的例子,簡(jiǎn)要地介紹Z語(yǔ)言。用Z語(yǔ)言描述的、最簡(jiǎn)單的形式化規(guī)格說(shuō)明含有下述4個(gè)部分:給定的集合、數(shù)據(jù)類型及常數(shù)。狀態(tài)定義。初始狀態(tài)。操作。2023/7/2345湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄1.給定的集合一個(gè)Z規(guī)格說(shuō)明從一系列給定的初始化集合開(kāi)始。所謂初始化集合就是不需要詳細(xì)定義的集合,這種集合用帶方括號(hào)的形式表示。對(duì)于電梯問(wèn)題,給定的初始化集合稱為Button,即所有按鈕的集合,因此,Z規(guī)格說(shuō)明開(kāi)始于：

[Button]2023/7/2346湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄2.狀態(tài)定義一個(gè)Z規(guī)格說(shuō)明由若干個(gè)“格(schema)”組成,每個(gè)格含有一組變量說(shuō)明和一系列限定變量取值范圍的謂詞。例如,格S的格式如圖4.12所示。在電梯問(wèn)題中,Button有4個(gè)子集,即floor_buttons(樓層按鈕的集合)、elevator_buttons(電梯按鈕的集合)、buttons(電梯問(wèn)題中所有按鈕的集合)以及pushed(所有被按的按鈕的集合,即所有處于打開(kāi)狀態(tài)的按鈕的集合)。圖4.13描述了格Button_State,其中,符號(hào)P表示冪集(即給定集的所有子集)。約束條件聲明,floor_buttons集與elevator_buttons集不相交,而且它們共同組成buttons集。2023/7/2347湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.12Z格S的格式2023/7/2348湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.13Z格Button_State2023/7/2349湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄3.初始狀態(tài)抽象的初始狀態(tài)是指系統(tǒng)第一次開(kāi)啟時(shí)的狀態(tài)。對(duì)于電梯問(wèn)題來(lái)說(shuō),抽象的初始狀態(tài)為：

Button_Init[Button_State｜pushed=]

上式表示,當(dāng)系統(tǒng)首次開(kāi)啟時(shí)pushed集為空,即所有按鈕都處于關(guān)閉狀態(tài)。2023/7/2350湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄4.操作如果一個(gè)原來(lái)處于關(guān)閉狀態(tài)的按鈕被按下,則該按鈕開(kāi)啟,這個(gè)按鈕就被添加到pushed集中。圖4.14定義了操作Push_Button(按按鈕)。Z語(yǔ)言的語(yǔ)法規(guī)定:當(dāng)一個(gè)格被用在另一個(gè)格中時(shí),要在它的前面加上三角形符號(hào)△作為前綴,因此,格Push_Button的第一行最前面有一個(gè)三角形符號(hào)作為格Button_State的前綴。操作Push_Button有一個(gè)輸入變量“button?”。問(wèn)號(hào)“?”表示輸入變量,而感嘆號(hào)“!”代表輸出變量。2023/7/2351湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

操作的謂詞部分,包含了一組調(diào)用操作的前置條件,以及操作完全結(jié)束后的后置條件。如果前置條件成立,則操作執(zhí)行完成后可得到后置條件。但是,如果在前置條件不成立的情況下調(diào)用該操作,則不能得到指定的結(jié)果(因此結(jié)果無(wú)法預(yù)測(cè))。2023/7/2352湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

圖4.14中的第一個(gè)前置條件規(guī)定,“button?”必須是buttons的一個(gè)元素,而buttons是電梯系統(tǒng)中所有按鈕的集合。如果第二個(gè)前置條件button?pushed得到滿足(即按鈕沒(méi)有開(kāi)啟),則更新pushed按鈕集,使之包含剛開(kāi)啟的按鈕“button?”。在Z語(yǔ)言中,當(dāng)一個(gè)變量的值發(fā)生改變時(shí),就用符號(hào)

'表示。也就是說(shuō),后置條件是當(dāng)執(zhí)行完操作Push_Button之后,“button?”將被加入到pushed集中。我們無(wú)需直接打開(kāi)按鈕,只要使“button?”變成pushed中的一個(gè)元素即可。2023/7/2353湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.14操作Push_Button的Z規(guī)格說(shuō)明2023/7/2354湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

還有一種可能性是,被按的按鈕原先已經(jīng)打開(kāi)了。由于button?∈pushed,根據(jù)第三個(gè)前置條件,將沒(méi)有任何事情發(fā)生,這可以用pushed’=pushed來(lái)表示,即pushed的新?tīng)顟B(tài)和舊狀態(tài)一樣。注意,如果沒(méi)有第三個(gè)前置條件,規(guī)格說(shuō)明將不能說(shuō)明在一個(gè)按鈕已被按過(guò)之后又被按了一次的情況下將發(fā)生什么事,因此,結(jié)果將是不可預(yù)測(cè)的。2023/7/2355湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄

假設(shè)電梯到達(dá)了某樓層,如果相應(yīng)的樓層按鈕已經(jīng)打開(kāi),則此時(shí)它會(huì)關(guān)閉；同樣,如果相應(yīng)的電梯按鈕已經(jīng)打開(kāi),則此時(shí)它也會(huì)關(guān)閉。也就是說(shuō),如果“button?”屬于pushed集,則將它移出該集合,如圖4.15所示(符號(hào)“＼”表示集合差運(yùn)算)。但是,如果按鈕“button?”原先沒(méi)有打開(kāi),則pushed集合不發(fā)生變化。2023/7/2356湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄圖4.15操作Floor_Arrival的Z規(guī)格說(shuō)明2023/7/2357湖南科技大學(xué)計(jì)算機(jī)學(xué)院戴祖雄4.4.2評(píng)價(jià)

Z語(yǔ)言之所以會(huì)獲得如此多的成功,主要有以下幾個(gè)原因:可以比