4.14.24.34.44.5第4章形式化說明技術(shù)概述有窮狀態(tài)機Petri網(wǎng)Z語言小結(jié)第一頁，編輯于星期一：十四點十八分。4.14.24.34.44.5第4章形式化說明技術(shù)概述有窮狀4.1概述?4.1.1非形式化方法的缺點?非形式化是指用自然語言描述軟件需求（如系統(tǒng)規(guī)格說明書）。因此，可能存在矛盾性、二義性、含糊性、不完整性、抽象層次混亂等問題。?4.1.2形式化方法的優(yōu)點?形式化方法是指在軟件工程中引入數(shù)學方法和模型。利用數(shù)學的簡潔性、嚴謹性、科學性，克服非形式化方法的缺點。?4.1.3應(yīng)用形式化方法的準則?“軟件需求”是軟件產(chǎn)品的高層、概念模型，而“形式化方法”是嚴謹、科學的數(shù)學方法，因此，在形式化方法的應(yīng)用方面應(yīng)考慮適度性、實用性、實用性。?常用的形式化方法?較嚴格的形式化方法（語法和語義都嚴謹）：有窮狀態(tài)機、言………Petri網(wǎng)、Z語?半形式化方法（語法和語義都不太嚴謹）據(jù)字典、圖、IPO表ER………圖、數(shù)據(jù)庫范式、狀態(tài)轉(zhuǎn)換圖、層次方框圖、：系統(tǒng)流程圖、數(shù)據(jù)流圖、數(shù)Warnier圖、IPO第二頁，編輯于星期一：十四點十八分。4.1概述?4.1.1非形式化方法的缺點?非形式化是指用自然4.1.1非形式化方法的缺點?矛盾性?在需求規(guī)格說明書（同的描述。ReqirementSpecifications）中對同一問題前后存在不?二義性?需求規(guī)格說明書的讀者對其中同一問題的描述存在不同的理解。?含糊性?需求規(guī)格說明書中對某一問題的描述不清晰、不可理解、不知如何實現(xiàn)、不具可操作性。?不完整性?需求規(guī)格說明書中對某一問題的描述不完整。只說明了局部，沒有說明整體；或者只說明了概要，未說明細節(jié)。因此不具可操作性。?抽象層次混亂?在不同層次的抽象模型中內(nèi)容混亂，如在高層模型中混有底層細節(jié)，造成讀者不能理解系統(tǒng)的整體功能和下級功能。第三頁，編輯于星期一：十四點十八分。4.1.1非形式化方法的缺點?矛盾性?在需求規(guī)格說明書（同的4.1.2形式化方法的優(yōu)點?可嚴謹?shù)孛枋鲕浖枨笾械膯栴}?可簡潔、準確描述物理現(xiàn)象、對象或動作的結(jié)果問題；適用于描述詳細的需求規(guī)格；可用數(shù)學方法驗證需求。?可在軟件工程不同階段平滑過渡?從需求、到設(shè)計、到實現(xiàn)都基于同一系統(tǒng)模型，平滑過渡。?可提供高層確認手段?可用數(shù)學方法證明軟件工程各階段的正確性（可回溯性），如“設(shè)計”符合“規(guī)格說明”、“編碼實現(xiàn)”符合“設(shè)計”。?形式化方法的適用性問題?形式化方法能較好地解決需求的“二義性”、“含糊性”問題。但不能解決需求的矛盾性、完整性等問題，這些問題涉及工程管理。第四頁，編輯于星期一：十四點十八分。4.1.2形式化方法的優(yōu)點?可嚴謹?shù)孛枋鲕浖枨笾械膯栴}?可4.1.3應(yīng)用形式化方法的準則?應(yīng)該選用適當?shù)囊?guī)格說明表示方法?應(yīng)該形式化，但不要過分形式化?應(yīng)該估算推行形式化的成本?應(yīng)該有形式化方法顧問隨時提供咨詢?應(yīng)該結(jié)合傳統(tǒng)的、證明有效的開發(fā)方法?應(yīng)該在采用形式化的同時，建立詳盡的文檔?應(yīng)該堅持質(zhì)量保障活動?應(yīng)該不總是盲目依賴形式化方法?應(yīng)該重視測試?應(yīng)該重視重用第五頁，編輯于星期一：十四點十八分。4.1.3應(yīng)用形式化方法的準則?應(yīng)該選用適當?shù)囊?guī)格說明表示4.2有窮狀態(tài)機?4.2.1?4.2.2?4.2.3有窮狀態(tài)機概念有窮狀態(tài)機例子有窮狀態(tài)機方法評價第六頁，編輯于星期一：十四點十八分。4.2有窮狀態(tài)機?4.2.1?4.2.2?4.2.3有窮狀態(tài)4.2.1有窮狀態(tài)機概念?通過簡單例子引入有窮狀態(tài)機的基本概念：一個保險箱上裝了一個復合鎖，鎖有三個位置，分別標記為1時刻轉(zhuǎn)盤都有、2、3，轉(zhuǎn)盤可向左和6種可能的運動，即(L)或向右1L(R)、轉(zhuǎn)動。這樣，在任意1R、2L、2R、3L他運動都將引起報警。3R。保險箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤的任何其?第七頁，編輯于星期一：十四點十八分。4.2.1有窮狀態(tài)機概念?通過簡單例子引入有窮狀態(tài)機的基本概引例——保險箱的狀態(tài)轉(zhuǎn)換?圖4.1保險箱的狀態(tài)轉(zhuǎn)換圖第八頁，編輯于星期一：十四點十八分。引例——保險箱的狀態(tài)轉(zhuǎn)換?圖4.1保險箱的狀態(tài)轉(zhuǎn)換圖第八頁引例——保險箱的狀態(tài)轉(zhuǎn)換第九頁，編輯于星期一：十四點十八分。引例——保險箱的狀態(tài)轉(zhuǎn)換第九頁，編輯于星期一：十四點十八分有窮狀態(tài)機——概念?一個有窮狀態(tài)機包括下述5個部分：狀態(tài)集J、輸入集K、由當前狀態(tài)和當前輸入確定下一個狀態(tài)(次態(tài))的轉(zhuǎn)換函數(shù)T、初始態(tài)S和終態(tài)集F。?狀態(tài)集J：由所有可能的狀態(tài)構(gòu)成的有窮集合；?輸入集K：引發(fā)狀態(tài)變換的可能的外部輸入（或操作）；?轉(zhuǎn)換函數(shù)T：由當前狀態(tài)和當前輸入變換到下一個狀態(tài)(次態(tài))的函數(shù)（或規(guī)則）；?初始態(tài)S∈J，狀態(tài)機的初始狀態(tài)；?終態(tài)集F∪J，狀態(tài)機的終止狀態(tài)集；第十頁，編輯于星期一：十四點十八分。有窮狀態(tài)機——概念?一個有窮狀態(tài)機包括下述5個部分：狀態(tài)集引例——保險箱的有窮狀態(tài)機?狀態(tài)集?J：｛保險箱鎖定，A，B，保險箱解鎖，報警｝。?輸入集K：?｛1L，1R，2L，2R，?轉(zhuǎn)換函數(shù)T：?見“狀態(tài)轉(zhuǎn)換表”?初始態(tài)S：?保險箱鎖定?終態(tài)集F：?｛保險箱解鎖，報警｝，3R｝。3L第十一頁，編輯于星期一：十四點十八分。引例——保險箱的有窮狀態(tài)機?狀態(tài)集?J：｛保險箱鎖定，A有窮狀態(tài)機——形式化表示?一個有窮狀態(tài)機可以表示為一個5元組(J，K，T，S，F(xiàn))，其中：?J是一個有窮的非空狀態(tài)集；?K是一個有窮的非空輸入集；?T是一個從(J-F)×K到J的轉(zhuǎn)換函數(shù)；?S∈J，是一個初始狀態(tài)；?F∪J，是終態(tài)集。第十二頁，編輯于星期一：十四點十八分。有窮狀態(tài)機——形式化表示?一個有窮狀態(tài)機可以表示為一個5元擴展的有窮狀態(tài)機——增加謂詞集?一個有窮狀態(tài)機可以表示為一個6元組(J,K,P,T,S,F)，其中：?J是一個有窮的非空狀態(tài)集；?K是一個有窮的非空輸入集；?P是一個有窮的非空謂詞集(條件函數(shù)集合)?T是一個從(J-F)×K×P到J的轉(zhuǎn)換函數(shù)；?S∈J，是一個初始狀態(tài)；?F∪J，是終態(tài)集。；第十三頁，編輯于星期一：十四點十八分。擴展的有窮狀態(tài)機——增加謂詞集?一個有窮狀態(tài)機可以表示為一個4.2.2有窮狀態(tài)機例子-電梯控制系統(tǒng)?自然語言描述的對電梯系統(tǒng)的需求?電梯系統(tǒng)有窮狀態(tài)機-按鈕集?電梯按鈕（電梯內(nèi)）的狀態(tài)轉(zhuǎn)換?樓層按鈕（電梯外）的狀態(tài)轉(zhuǎn)換第十四頁，編輯于星期一：十四點十八分。4.2.2有窮狀態(tài)機例子-電梯控制系統(tǒng)?自然語言描述的對電梯自然語言描述的對電梯系統(tǒng)的需求?在一幢m層的大廈中需要一套控制n部電梯的產(chǎn)品，要求這n部電梯按照約束條件C1，C2和C3在樓層間移動。?C1：每部電梯內(nèi)有m個按鈕，每個按鈕代表一個樓層。當按下一個按鈕時該按鈕指示燈亮，同時電梯駛向相應(yīng)的樓層，到達按鈕指定的樓層時指示燈熄滅。?C2：除了大廈的最低層和最高層之外，每層樓（電梯外）都有兩個按鈕分別請求電梯上行和下行。這兩個按鈕之一被按下時相應(yīng)的指示燈亮，當電梯到達此樓層時燈熄滅，電梯向要求的方向移動。?C3：當對電梯沒有請求時，它關(guān)門并停在當前樓層。第十五頁，編輯于星期一：十四點十八分。自然語言描述的對電梯系統(tǒng)的需求?在一幢m層的大廈中需要一套電梯系統(tǒng)有窮狀態(tài)機-按鈕集?現(xiàn)在使用一個擴展的有窮狀態(tài)機對本產(chǎn)品進行規(guī)格說明。這個問題中有兩個按鈕集：?在層。因為這n部電梯中，每一部都鈕。m×n個按鈕都在電梯中，所以稱它們?yōu)橛衜個按鈕，一個按鈕對應(yīng)一個樓電梯按?此外，每層樓有兩個按鈕（底樓、頂樓均只有一個）請求向上，另一個請求向下，這些按鈕稱為樓層按鈕。，一個第十六頁，編輯于星期一：十四點十八分。電梯系統(tǒng)有窮狀態(tài)機-按鈕集?現(xiàn)在使用一個擴展的有窮狀態(tài)機對本電梯按鈕的狀態(tài)轉(zhuǎn)換（圖）?令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ā)光且電梯到達f層，該按鈕將熄滅。相反如果按鈕熄滅，則按下它時，按鈕將發(fā)光。上述描述中包含了兩個事件，它們分別是：?EBP(e,f)：電梯按鈕(e,f)被按下?EAF(e,f)：電梯e到達f層第十七頁，編輯于星期一：十四點十八分。電梯按鈕的狀態(tài)轉(zhuǎn)換（圖）?令EB(e,f)表示按下電梯e電梯按鈕狀態(tài)轉(zhuǎn)換的相關(guān)謂詞?為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，需要一個謂詞V(e,f)，它的含義如下：?V(e,f)：電梯e停在f層?如果電梯按鈕(e,f)處于關(guān)閉狀態(tài)〔當前狀態(tài)〕，而且電梯按鈕(e,f)被按下〔事件〕，而且電梯e不在f層〔謂詞〕，則該電梯按鈕打開發(fā)光〔下個狀態(tài)〕。狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下：?EBOFF(e,f)+EBP(e,f)+notV(e,f)=>EBON(e,f)?反之，如果電梯到達f層，而且電梯按鈕是打開的，于是它就會熄滅。這條轉(zhuǎn)換規(guī)則可以形式化地表示為：?EBON(e,f)+EAF(e,f)=>EBOFF(e,f)第十八頁，編輯于星期一：十四點十八分。電梯按鈕狀態(tài)轉(zhuǎn)換的相關(guān)謂詞?為了定義與這些事件和狀態(tài)相聯(lián)系的樓層按鈕的狀態(tài)轉(zhuǎn)換（圖）?令FB(d,f)表示f層請求電梯向d方向運動的按鈕，樓層按鈕FB(d,f)的狀態(tài)轉(zhuǎn)換圖如圖所示。樓層按鈕的狀態(tài)如下：?FBON(d,f)：樓層按鈕(d,f)打開?FBOFF(d,f)：樓層按鈕(d,f)關(guān)閉?如果樓層按鈕已經(jīng)打開，而且一部電梯到達f層，則鈕關(guān)閉。反之，如果樓層按鈕原來是關(guān)閉的，被按下后該按鈕將打開。這段敘述中包含了以下兩個事件。?FBP(d,f)：樓層按鈕(d,f)被按下?EAF(1…n,f)或為n。：電梯1或…或n到達f層，其中1…n表示或為1或為2…第十九頁，編輯于星期一：十四點十八分。樓層按鈕的狀態(tài)轉(zhuǎn)換（圖）?令FB(d,f)表示f層請求電樓層按鈕狀態(tài)轉(zhuǎn)換的相關(guān)謂詞?為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，同樣也需要一個謂詞S(d,e,f)，它的定義如下。?S(d,e,f)：電梯e停在f層并且移動方向由d確定為向上(d=U)或向下(d=D)或待定(d=N)。?這個謂詞實際上是一個狀態(tài)，形式化方法允許把事件和狀態(tài)作為謂詞對待。使用謂詞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。?也就是說:?如果在被按下，并且當時沒有正停在f層請求電梯向d方向運動的樓層按鈕處于關(guān)閉狀態(tài)，現(xiàn)在該按鈕鈕打開。f層準備向d方向移動的電梯，則該樓層按?反之，如果樓層按鈕已經(jīng)打開，且至少有一部電梯將朝d方向運動，則按鈕將關(guān)閉。梯到達f層，且該部電第二十頁，編輯于星期一：十四點十八分。樓層按鈕狀態(tài)轉(zhuǎn)換的相關(guān)謂詞?為了定義與這些事件和狀態(tài)相聯(lián)系的V(e,f)重新定義?討論電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時定義的謂詞V(e,f)（電梯e停在f層），可以用謂詞S(d,e,f)重新定義如下：?V(e,f)=S(U,e,f)orS(D,e,f)orS(N,e,f)第二十一頁，編輯于星期一：十四點十八分。V(e,f)重新定義?討論電梯按鈕狀態(tài)轉(zhuǎn)換規(guī)則時定義的謂詞V電梯的狀態(tài)、事件及轉(zhuǎn)換規(guī)則?電梯的3個狀態(tài)：???M(d,e,f)：電梯e正沿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ā)傳感器，電梯控制器決定在當前樓層電梯是否停?RL：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)(這里給出的規(guī)則僅發(fā)生在關(guān)門之時)：?S(U,e,f)+DC(e,f)=>M(U,e,f+1)：?如果電梯e停在f層準備向上(U)移動，且門已經(jīng)關(guān)閉，則電梯將向上一樓層移動。?S(D,e,f)+DC(e,f)=>M(D,e,f-1)?如果電梯e停在f層準備向下(D)移動，且門已經(jīng)關(guān)閉，則電梯將向下一樓層移動。?S(N,e,f)+DC(e,f)=>W(e,f)。?如果電梯e停在f層沒有移動請求(N)，且門已經(jīng)關(guān)閉，則電梯等待移動。電梯的電梯的狀態(tài)轉(zhuǎn)換規(guī)則第二十二頁，編輯于星期一：十四點十八分。電梯的狀態(tài)、事件及轉(zhuǎn)換規(guī)則?電梯的3個狀態(tài)：???M(d,電梯的狀態(tài)轉(zhuǎn)換圖電梯被控電梯電上梯行下中行中電梯等待中第二十三頁，編輯于星期一：十四點十八分。電梯的狀態(tài)轉(zhuǎn)換圖電梯被控電梯電上梯行下中行中電梯等待中第二十4.2.3有窮狀態(tài)機方法評價（特點）?采用一種簡單的有窮狀態(tài)機方法格式來描述規(guī)格說明：?當前狀態(tài)+事件+謂詞=>下個狀態(tài)?這種形式的規(guī)格說明易于書寫、易于驗證。?有窮狀態(tài)機可以比較容易地把它轉(zhuǎn)變成設(shè)計或程序代碼：?可開發(fā)一個護可以通過重新轉(zhuǎn)變來實現(xiàn)，也就是說，如果需要一個新的狀態(tài)或事件CASE工具把一個有窮狀態(tài)機規(guī)格說明直接轉(zhuǎn)變?yōu)樵创a。維，首先修改規(guī)格說明，然后直接由新的規(guī)格說明生成新版本的產(chǎn)品。?有窮狀態(tài)機方法與數(shù)據(jù)流圖技術(shù)比較?有窮狀態(tài)機描述需求比數(shù)據(jù)流圖技術(shù)更精確；?與數(shù)據(jù)流圖一樣易于理解（還是要難一點）。?有窮狀態(tài)機存在的缺點：?在開發(fā)一個大系統(tǒng)時三元組(即狀態(tài)、事件、謂詞)的數(shù)量會迅速增長。?和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機方法（下節(jié)將介紹的Petri網(wǎng)技術(shù)，是一種可處理定時問題的形式化方法。）也沒有處理定時需求。第二十四頁，編輯于星期一：十四點十八分。4.2.3有窮狀態(tài)機方法評價（特點）?采用一種簡單的有窮狀態(tài)4.3Petri網(wǎng)?4.3.1?4.3.2?4.3.3Petri網(wǎng)概念Petri網(wǎng)例子Petri網(wǎng)方法評價第二十五頁，編輯于星期一：十四點十八分。4.3Petri網(wǎng)?4.3.1?4.3.2?4.3.3Pe4.3.1Petri網(wǎng)概念?軟件系統(tǒng)的定時問題?Petri網(wǎng)及其用途?Petri網(wǎng)的構(gòu)成?Petri網(wǎng)的形式化表示第二十六頁，編輯于星期一：十四點十八分。4.3.1Petri網(wǎng)概念?軟件系統(tǒng)的定時問題?Petri軟件系統(tǒng)的定時問題?并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題。這個問題可以表現(xiàn)為多種形式，如同步問題、競爭條件以及死鎖問題。?定時出現(xiàn)問題通常是由不好的設(shè)計或有錯誤的實現(xiàn)引起的，而這樣的設(shè)計或?qū)崿F(xiàn)通常又是由不好的規(guī)格說明造成的。如果規(guī)格說明不恰當，則有導致不完善的設(shè)計或?qū)崿F(xiàn)的危險。第二十七頁，編輯于星期一：十四點十八分。軟件系統(tǒng)的定時問題?并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題。Petri網(wǎng)及其用途?用于確定系統(tǒng)中隱含的定時問題的一種有效技術(shù)是Petri網(wǎng)，這種技術(shù)的一個很大的優(yōu)點是它也可以用于設(shè)計中，有效地描述并發(fā)活動。?Petri網(wǎng)是對離散并行系統(tǒng)的數(shù)學表示。Petri網(wǎng)既有嚴格的數(shù)學表述方式，也有直觀的圖形表達方式。?Petri網(wǎng)適合于描述異步的、并發(fā)的自動化系統(tǒng)和計算機系統(tǒng)模型。Petri網(wǎng)在計算機科學中得到了廣泛的應(yīng)用，例如，在系統(tǒng)性能評價、操作系統(tǒng)和軟件工程等領(lǐng)域，Petri網(wǎng)應(yīng)用得都比較廣泛。第二十八頁，編輯于星期一：十四點十八分。Petri網(wǎng)及其用途?用于確定系統(tǒng)中隱含的定時問題的一種有效Petri網(wǎng)的構(gòu)成?Petri網(wǎng)包含????4種元素：一組位置P(Place):圓圈一組轉(zhuǎn)換T(Transition):短直線輸入函數(shù)I(Input)輸出函數(shù)O(Output)?其他元素???例?P:｛P1,P2,P3,P4｝?T:｛t1,t2｝?I:I(t1)=｛P2,P4｝,I(t2)=｛P2｝?O:O(t1)=｛P1｝O(t2)=｛P3，P3}連接Connection:箭頭權(quán)標Token(令牌):圓點第二十九頁，編輯于星期一：十四點十八分。Petri網(wǎng)的構(gòu)成?Petri網(wǎng)包含????4種元素：一Petri網(wǎng)的形式化表示?一個Petri網(wǎng)是一個四元組C?C=(P,T,I,O)?其中:?P=｛P1，…，Pn｝是一個有窮位置集，n≥0。?T=不相交。｛t1，…，tm｝是一個有窮轉(zhuǎn)換集，m≥0，且T和P?I映射。：T→P∞為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組(bags)的?O。：T→P∞為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射?一個無序單位組（或多重組）是允許一個元素有多個實例的廣義集第三十頁，編輯于星期一：十四點十八分。Petri網(wǎng)的形式化表示?一個Petri網(wǎng)是一個四元組C?CPetri網(wǎng)的標記?權(quán)標(token，令牌)?Petri繼轉(zhuǎn)換網(wǎng)位置t的條件。P中的權(quán)標（用圓點表示），表示該位置持有的可激發(fā)與其連接的后?標記（M，Mark）?位置Petri網(wǎng)的標記是在P到一組非負整數(shù)的映射，即Petri網(wǎng)中權(quán)標(token，令牌)的分配。Petri網(wǎng)標記M是由一組M：P→｛0，1，2，…｝?其中的數(shù)字表示每個位置中當前的權(quán)標數(shù)量。?轉(zhuǎn)換的激發(fā)?通常，當每個輸入位置所擁有的權(quán)標數(shù)大于等于從該位置到所直接連接的后續(xù)轉(zhuǎn)換標（用掉了t的線數(shù)時，就允許激發(fā)該轉(zhuǎn)換1個）；t所直接連接的后續(xù)位置增加一個權(quán)標（獲得了t。此時，t所直接連接的前序位置減少一個權(quán)1個）。?Petri網(wǎng)具有非確定性，也就是說，如果數(shù)個轉(zhuǎn)換都達到了激發(fā)條件，則其中任意一個都可以被激發(fā)。第三十一頁，編輯于星期一：十四點十八分。Petri網(wǎng)的標記?權(quán)標(token，令牌)?Petri繼例：帶權(quán)標的Petri網(wǎng)?在圖4.6中有4個權(quán)標，其中一個在P1中，兩個在P2中，P3中沒有，還有一個在P4中。上述標記可以用向量(1,2,0,1）表示。?由于P2和P4中有權(quán)標，因此t1啟動(即被激發(fā))。當t1被激發(fā)時，P2和P4上各有一個權(quán)標被移出，而P1上則增加一個權(quán)標。Petri網(wǎng)中權(quán)標總數(shù)不是固定的，在這個例子中兩個權(quán)標被移出，而P1上只能增加一個權(quán)標。圖4.6帶標記的Petri網(wǎng)圖4.7Petri網(wǎng)在轉(zhuǎn)換t1被激發(fā)后的情況第三十二頁，編輯于星期一：十四點十八分。例：帶權(quán)標的Petri網(wǎng)?在圖4.6中有4個權(quán)標，其中一例：帶權(quán)標的Petri網(wǎng)（續(xù)）?在圖4.6中P2上有權(quán)標，因此t2也可以被激發(fā)。當t2被激發(fā)時，P2上將移走一個權(quán)標，而P3上新增加兩個權(quán)標。圖4.6所示Petri網(wǎng)的標記為(1，2，0，1)，t1和t2都可以被激發(fā)。假設(shè)t1被激發(fā)了，則結(jié)果如圖4.7所示，標記為(2，1，0，0)。此時，只有t2可以被激發(fā)。如果t2也被激發(fā)了，則權(quán)標從P2中移出，兩個新權(quán)標被放在P3上，結(jié)果如圖4.8所示，標記為(2，0，2，0)。圖4.7Petri網(wǎng)在轉(zhuǎn)換t1被激發(fā)后的情況圖4.8圖4.7的Petri網(wǎng)在轉(zhuǎn)換t2被激發(fā)后的情況第三十三頁，編輯于星期一：十四點十八分。例：帶權(quán)標的Petri網(wǎng)（續(xù)）?在圖4.6中P2上有權(quán)標含禁止線的Petri網(wǎng)?禁止線是使用“圓點”（而不是箭頭）標記的輸入線。表示禁止線上（圖中P2）沒有權(quán)標時，后續(xù)的轉(zhuǎn)換（圖中t1）才可激活。?圖4.9例：箭頭線P3上有權(quán)標，而禁止線P2上沒有權(quán)標，所以轉(zhuǎn)換t1可以激活。圖4.9含禁止線的Petri網(wǎng)第三十四頁，編輯于星期一：十四點十八分。含禁止線的Petri網(wǎng)?禁止線是使用“圓點”（而不是箭頭）標更形式化的Petri網(wǎng)定義（增加標記M）?一個Petri網(wǎng)是一個五元組C?C=(P，T，I，O，M)?其中:?P=｛P1，…，Pn｝?是一個有窮位置集，n≥0。?T=｛t1，…，tm｝?是一個有窮轉(zhuǎn)換集，m≥0，且T和P不相交。?I：T→P∞?為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組(bags)的映射。?O：T→P∞?為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射。?M：P→｛0，1，2，…｝?是由一組位置P到一組非負整數(shù)的映射第三十五頁，編輯于星期一：十四點十八分。更形式化的Petri網(wǎng)定義（增加標記M）?一個Petri網(wǎng)是4.3.2Petri網(wǎng)例子：電梯系統(tǒng)控制?Petri網(wǎng)應(yīng)用于電梯問題?當用明時，每個樓層用一個位置Petri網(wǎng)表示上一節(jié)討論過的電梯系統(tǒng)的規(guī)格說Ff代表(1≤f≤m)；?在權(quán)標，表示在樓層Petri網(wǎng)中電梯是用一個權(quán)標代表的。在位置f上有電梯。Ff上有?可能的幾種約束條件?電梯按鈕（約束條件C1，電梯內(nèi)有按鈕操作）?樓層按鈕（約束條件C2，樓層中有按鈕操作）?電梯靜止（約束條件C3，沒有任何操作請求）第三十六頁，編輯于星期一：十四點十八分。4.3.2Petri網(wǎng)例子：電梯系統(tǒng)控制?Petri網(wǎng)應(yīng)用于1.電梯按鈕（約束條件C1）?第一個約束條件C1，描述了“電梯按鈕”的行為：?每部電梯有m個按鈕，每層對應(yīng)一個按鈕。?當按下一個按鈕時該按鈕指示燈亮，指示電梯移往相應(yīng)的樓層。?當電梯到達指定的樓層時，按鈕將熄滅。?為了用Petri網(wǎng)表達電梯按鈕的規(guī)格說明，在Petri網(wǎng)中還必須設(shè)置其他的“電梯按鈕位置”：?電梯中樓層f的按鈕，在Petri網(wǎng)中用位置EBf表示(1≤f≤m)?在EBf上有一個權(quán)標，就表示電梯內(nèi)樓層f的按鈕被按下了。?電梯按鈕只有在第一次被按下時才會由暗變亮，以后再按它則只會被忽略。第三十七頁，編輯于星期一：十四點十八分。1.電梯按鈕（約束條件C1）?第一個約束條件C1，描述了“電梯按鈕的Petri網(wǎng)?圖4.10所示的Petri網(wǎng)準確地描述了電梯按鈕的行為規(guī)律：?線的情況下，轉(zhuǎn)換“首先，假設(shè)按鈕沒有發(fā)亮，顯然在位置EBf上沒有權(quán)標，從而在存在禁止換被激發(fā)并在EBf上放置了一個權(quán)標。EBf被按下”是允許發(fā)生的。假設(shè)現(xiàn)在按下按鈕，則轉(zhuǎn)?“以后不論再按下多少次按鈕，禁止線與現(xiàn)有權(quán)標的組合都決定了轉(zhuǎn)換EBf被按下”不能再被激發(fā)了，因此，位置EBf上的權(quán)標數(shù)不會多于1。圖4.10Petri網(wǎng)表示的電梯按鈕第三十八頁，編輯于星期一：十四點十八分。電梯按鈕的Petri網(wǎng)?圖4.10所示的Petri網(wǎng)準確地描電梯按鈕的Petri網(wǎng)（續(xù)）?續(xù)：?假設(shè)電梯由各有一個權(quán)標，轉(zhuǎn)換“電梯在運行”被激發(fā)，從而g層駛向f層，因為電梯在g層，位置Fg有一個權(quán)標。由于每條輸入線上EBf和Fg上的權(quán)標被移走，按鈕Bf關(guān)閉，在位置Ff上出現(xiàn)一個新權(quán)標，即轉(zhuǎn)換的激發(fā)使電梯由g層駛到f層。?事實上，電梯由如，由于物理上的原因按鈕被按下后不能馬上發(fā)亮g層移到f層是需要時間的，為處理這個情況及其他類似的問題。也就是說，在標準)(例制Petri網(wǎng)，以使轉(zhuǎn)換與非零時間相聯(lián)系。Petri網(wǎng)中轉(zhuǎn)換是瞬時完成的，而在現(xiàn)實情況下就需要時間控，Petri網(wǎng)模型中必須加入時限圖4.10Petri網(wǎng)表示的電梯按鈕第三十九頁，編輯于星期一：十四點十八分。電梯按鈕的Petri網(wǎng)（續(xù)）?續(xù)：?假設(shè)電梯由各有一個權(quán)標，2.樓層按鈕（約束條件C2）?第二條約束C2，描述了樓層按鈕的行為：?電梯上行，另一個要求電梯下行。這些按鈕在按下時發(fā)亮，除了第一層與頂層之外，每個樓層都有兩個按鈕，一個要求當電梯到達該層并將向指定方向移動時，相應(yīng)的按鈕才會熄滅。?在Petri網(wǎng)中樓層按鈕位置：?電梯上行和下行的按鈕。Petri網(wǎng)中樓層按鈕用位置FBfu和FBfd表示，分別代表f樓層請求?個按鈕底層的按鈕為FBFB1u，最高層的按鈕為FBmd，中間每一層有兩fu和FBfd(1＜f＜m)。第四十頁，編輯于星期一：十四點十八分。2.樓層按鈕（約束條件C2）?第二條約束C2，描述了樓層按樓層按鈕的Petri網(wǎng)（圖）圖4.11Petri網(wǎng)表示樓層按鈕第四十一頁，編輯于星期一：十四點十八分。樓層按鈕的Petri網(wǎng)（圖）圖4.11Petri網(wǎng)表示樓層樓層按鈕的Petri網(wǎng)?圖4.11所示的情況為電梯由g層駛向f層。根據(jù)電梯乘客的要求，某一個樓層按鈕亮或兩個樓層按鈕都亮。如果兩個按鈕都亮了，則只有一個按鈕熄滅。圖4.11所示的Petri網(wǎng)可以保證，當兩個按鈕都亮了的時候，只有一個按鈕熄滅。但是要保證按鈕熄滅正確，則需要更復雜的Petri網(wǎng)模型。第42頁/共62頁第四十二頁，編輯于星期一：十四點十八分。樓層按鈕的Petri網(wǎng)?圖4.11所示的情況為電梯由g層駛向電梯靜止條件（約束條件C3）?最后，考慮第三條約束C3：?當電梯沒有收到請求時，它將停留在當前樓層并關(guān)門。?這條約束很容易實現(xiàn)，如下圖所示，當沒有請求(FBFBfu和d不能被激發(fā)，而是停留在當前層（f上無權(quán)標）時，任何一個轉(zhuǎn)換“電梯在運行”都Fg）。第四十三頁，編輯于星期一：十四點十八分。電梯靜止條件（約束條件C3）?最后，考慮第三條約束C3：?當4.3.3Petri網(wǎng)方法評價?Petri網(wǎng)是1960年代由C.A.佩特里發(fā)明的，Petri網(wǎng)是對離散并行系統(tǒng)的數(shù)學表示。?Petri網(wǎng)適合于描述異步的、并發(fā)的計算機系統(tǒng)模型。?Petri網(wǎng)既有嚴格的數(shù)學表述方式，也有直觀的圖形表達方式。?由于Petri網(wǎng)能表達并發(fā)的事件，被認為是自動化理論的一種。研究領(lǐng)域趨向認為Petri網(wǎng)是所有流程定義語言之母。第四十四頁，編輯于星期一：十四點十八分。4.3.3Petri網(wǎng)方法評價?Petri網(wǎng)是1960年代由4.4Z語言?4.4.1?4.4.1?4.4.2Z語言簡介Z語言例子Z語言評價第四十五頁，編輯于星期一：十四點十八分。4.4Z語言?4.4.1?4.4.1?4.4.2Z語言簡介Z4.4.1Z語言簡介?????Z語言是由牛津大學程序設(shè)計研究小組開發(fā)的一種描述形式語言，在ISO指導下的國際標準化Z工作于2002年完成。Z語言中的“Z”指的是著名數(shù)學家Zermelo。Z語言是目前使用最廣泛的一種形式化描述語言，Z語言將事物的狀態(tài)和行為用數(shù)學符號形式化表達的語言，為編寫計算機程序和驗證計算機程序的正確性提供依據(jù)，是軟件工程中編碼之前的規(guī)格說明語言。Z語言在軟件產(chǎn)業(yè)的一些大型項目中已經(jīng)獲得成功的應(yīng)用，。Z語言是一種以一階謂詞演算為主要理論基礎(chǔ)的規(guī)約語言,是一種功能性語言。Z以帶等詞的一階謂詞邏輯ZF（Zermelo-Fraenkel，蔡梅羅-弗蘭科爾）公理集合論為主要數(shù)學基礎(chǔ)。在Z中有兩種語言：數(shù)學語言和模式（Schema）語言。數(shù)學語言用來描述系統(tǒng)的各種特征：對象及其之間的關(guān)系。模式語言是一種半圖形化的語言，它用來構(gòu)造、組織形式化說明的描述、整理、封裝信息塊并對其命名以便可以重用這些信息塊。通常，形式化說明的可讀性都不太好，但由于Z采用半圖形化的模式語言，能用一種比較直觀、有條理的方式來表達形式化說明，這就改善了可讀性。第四十六頁，編輯于星期一：十四點十八分。4.4.1Z語言簡介?????Z語言是由牛津大學程序設(shè)計研Z語言的需求規(guī)格說明的構(gòu)成?用Z語言描述的、最簡單的形式化規(guī)格說明含有下述4個部分：?給定的集合、數(shù)據(jù)類型及常數(shù)。?狀態(tài)定義。?初始狀態(tài)。?操作。第四十七頁，編輯于星期一：十四點十八分。Z語言的需求規(guī)格說明的構(gòu)成?用Z語言描述的、最簡單的形式化規(guī)1.給定的集合?給定的集合?集合就是不需要詳細定義的集合，這種集合用帶方括號的形式一個Z規(guī)格說明從一系列給定的初始化集合開始。所謂初始化表示。?電梯控制系統(tǒng)的“給定的集合”?合，因此，電梯問題中給定的初始化集合稱為Z規(guī)格說明開始于：Button，即所有按鈕的集?〔Button〕第四十八頁，編輯于星期一：十四點十八分。1.給定的集合?給定的集合?集合就是不需要詳細定義的集合，2.狀態(tài)定義?狀態(tài)定義——Z格?一個Z規(guī)格說明由若干個“格(schema)”組成，Z格的格式如圖4.12所示。?Z格由以下幾個部分構(gòu)成：?格的名稱（如：“S”）；?一組說明（Declarations），給出Z格中可能用到的變量；?一組謂詞（Predicates），限定變量取值范圍的。圖4.12Z格S的格式第四十九頁，編輯于星期一：十四點十八分。2.狀態(tài)定義?狀態(tài)定義——Z格?一個Z規(guī)格說明由若干個“格電梯控制系統(tǒng)中的Z格：Button_State（圖）變量說明（集合）謂詞（約束條件）圖4.13Z格Button_State第五十頁，編輯于星期一：十四點十八分。電梯控制系統(tǒng)中的Z格：Button_State（圖）變量說明電梯控制系統(tǒng)中的Z格：Button_State?電梯系統(tǒng)Z格中的說明——Button有4個子集：?floor_buttons(樓層按鈕的集合)?elevator_buttons(電梯按鈕的集合)?buttons(電梯問題中所有按鈕的集合)?pushed(的集合)所有被按的按鈕的集合，即所有處于打開狀態(tài)的按鈕。?符號P表示冪集(即給定集的所有子集)?(集，把它們放于圖在下面的討論中并不需要4.13中只是用來說明floor_buttonsZ集和格包含的內(nèi)容elevator_buttons)?電梯系統(tǒng)Z格中的謂詞——約束條件聲明:?floor_buttons集與elevator_buttons集不相交;?而且它們共同組成buttons集。第五十一頁，編輯于星期一：十四點十八分。電梯控制系統(tǒng)中的Z格：Button_State?電梯系統(tǒng)Z格3.初始狀態(tài)?初始狀態(tài)?抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。?電梯控制系統(tǒng)的抽象初始狀態(tài)為：?Button_Init??Button_State｜pushed=Φ〕?上式表示，當系統(tǒng)首次開啟時處于關(guān)閉狀態(tài)。pushed集為空，即所有按鈕都第五十二頁，編輯于星期一：十四點十八分。3.初始狀態(tài)?初始狀態(tài)?抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時4.操作????Z規(guī)格說明中的操作?描述了需求的操作，包括操作涉及到的變量、操作的前提（前置條件）以及操作的結(jié)果（后置條件）。操作的說明部分?操作的說明部分定義了該操作涉及到的輸入、輸出變量。操作的謂詞部分?操作的謂詞部分包含了一組調(diào)用操作的前置條件，以及操作完全結(jié)束后的后置條件。如果前置條件成立，則操作執(zhí)行完成后可得到后置條件。但是，如果在前置條件不成立的情況下調(diào)用該操作，則不能得到指定的結(jié)果(因此結(jié)果無法預測)。運算符&表達式?△格名——在本格中引用的格；?變量名？、變量名！——輸入變量、輸出變量；?邏輯運算符（∧、∨、…）；?集合運算符（∈、∪、∩、＼、…）；?變量名‘——變化后的變量。圖4.14操作Push_Button的Z規(guī)格說明第五十三頁，編輯于星期一：十四點十八分。4.操作????Z規(guī)格說明中的操作?描述了需求的操作，包括???電梯控制系統(tǒng)的操作：Push_Button圖4.14定義了“按下按鈕”操作Push_Button?如果一個原來處于關(guān)閉狀態(tài)的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到中。pushed集操作的說明部分?該操作中引用了外部Z格△Button_State；?該操作的輸入變量為Button？。操作的謂詞部分?第一個前置條件：輸入變量button？∈buttons（所有按鈕的集合）；?第二個前置條件：輸入變量button？不屬于pushed，則在pushed集合中增加該按鈕；?第三個前置條件：輸入變量）。如果沒有該條件，后果無法預測！button？屬于pushed，則pushed保持不變（操作前后狀態(tài)一樣圖4.14操作Push_Button的Z規(guī)格說明第五十四頁，編輯于星期一：十四點十八分。???電梯控制系統(tǒng)的操作：Push_Button圖4.14定電梯控制系統(tǒng)的操作：Floor_Arrival?操作Floor_Arrival假設(shè)電梯到達了某樓層，如果相應(yīng)的樓層按鈕已經(jīng)打開，則此時它會關(guān)閉；同樣，如果相應(yīng)的電梯按鈕已經(jīng)打開，則此時它也會關(guān)閉。也就是說，如果“則將它移出該集合，如圖4.15。button?”屬于pushed集，圖4.15操作Floor_Arrival的Z規(guī)格說明?第五十五頁，編輯于星期一：十四點十八分。電梯控制系統(tǒng)的操作：Floor_Arrival?操作Floo4.4.2評價?使用形式化規(guī)格說明是全球的總趨勢。目前，Z也許是應(yīng)用得最廣泛的形式化語言，尤其是在大型項目中Z語言的優(yōu)勢更加明顯。已經(jīng)在許多軟件開發(fā)項目中成功地運用了Z語言。?Z語言之所以會獲得如此多的成功，有諸多的原因和特點（下頁）。第五十六頁，編輯于星期一：十四點十八分。4.4.2評價?使用形式化規(guī)格說明是全球的總趨勢。目前，Z語言的主要優(yōu)點及特點?(1)易于發(fā)現(xiàn)規(guī)格說明中的錯誤??????據(jù)形式化的規(guī)格說明來審查設(shè)計與代碼時，情況更是如此?？梢员容^容易地發(fā)現(xiàn)用Z寫的規(guī)格說明的錯誤，特別是在自己審查規(guī)格說明，及根可精確地描述規(guī)格說明?，從而和非形式化規(guī)格說明相比，減少了模糊性、不一致性和遺漏。用Z寫規(guī)格說明時，要求作者十分精確地使用Z說明符。由于對精確性的要求很高方便需求說明的正確性驗證?Z是一種形式化語言，在需要時開發(fā)者可以嚴格地驗證規(guī)格說明的正確性。具有一定的可掌握性?仍然可以只用比較短的時間就學會編寫雖然完全學會Z語言相當困難，但是，經(jīng)驗表明，只學過中學數(shù)學的軟件開發(fā)人員規(guī)格說明的結(jié)果是否正確。Z規(guī)格說明，當然，這些人還沒有能力證明可降低軟件開發(fā)費用?式化技術(shù)要多，但開發(fā)過程所需要的總時間卻減少了。使用Z語言可以降低軟件開發(fā)費用。雖然用Z寫規(guī)格說明所需用的時間比使用非形易于正確地轉(zhuǎn)換成自然語言描述?規(guī)格說明。經(jīng)驗證明，這樣得到的自然語言規(guī)格說明，比直接用自然語言寫出的非雖然用戶無法理解用Z寫的規(guī)格說明，但是，可以依據(jù)Z規(guī)格說明用自然語言重寫形式化規(guī)格說明更清楚、更正確。(2)(3)(4)(5)(6)第五十七頁，編輯于星期一：十四點十八分。Z語言的主要優(yōu)點及特點?(1