這是一個關于軟件工程導論ppt，主要介紹有窮狀態(tài)機、Petri網、Z語言。第4章 形式化說明技術 4.1 概述 4.2 有窮狀態(tài)機 4.3 Petri網 4.4 Z語言 4.5 小結習題 按照形式化的程度，可以把軟件工程使用的方法劃分成非形式化、半形式化和形式化3類。用自然語言描述需求規(guī)格說明，是典型的非形式化方法。用數據流圖或實體-聯系圖建立模型，是典型的半形式化方法。所謂形式化方法，是描述系統性質的基于數學的技術，也就是說，如果一種方法有堅實的數學基礎，那么它就是形式化的。 4.1 概述 4.1.1 非形式化方法的缺點用自然語言書寫的系統規(guī)格說明書，可能存在矛盾、二義性、含糊性、不完整性及抽象層次混亂等問題。所謂矛盾是指一組相互沖突的陳述。二義性是指讀者可以用不同方式理解的陳述。 系統規(guī)格說明書是很龐大的文檔，因此，幾乎不可避免地會出現含糊性。實際上，這樣籠統的陳述并沒有給出任何有用的信息。不完整性可能是在系統規(guī)格說明中最常遇到的問題之一。抽象層次混亂是指在非常抽象的陳述中混進了一些關于細節(jié)的低層次陳述，歡迎點擊下載軟件工程導論ppt哦。

軟件工程導論ppt是由紅軟PPT免費下載網推薦的一款學校PPT類型的PowerPoint.

第4章 形式化說明技術 4.1 概述 4.2 有窮狀態(tài)機 4.3 Petri網 4.4 Z語言 4.5 小結習題 按照形式化的程度，可以把軟件工程使用的方法劃分成非形式化、半形式化和形式化3類。用自然語言描述需求規(guī)格說明，是典型的非形式化方法。用數據流圖或實體-聯系圖建立模型，是典型的半形式化方法。所謂形式化方法，是描述系統性質的基于數學的技術，也就是說，如果一種方法有堅實的數學基礎，那么它就是形式化的。 4.1 概述 4.1.1 非形式化方法的缺點用自然語言書寫的系統規(guī)格說明書，可能存在矛盾、二義性、含糊性、不完整性及抽象層次混亂等問題。所謂矛盾是指一組相互沖突的陳述。二義性是指讀者可以用不同方式理解的陳述。 系統規(guī)格說明書是很龐大的文檔，因此，幾乎不可避免地會出現含糊性。實際上，這樣籠統的陳述并沒有給出任何有用的信息。不完整性可能是在系統規(guī)格說明中最常遇到的問題之一。抽象層次混亂是指在非常抽象的陳述中混進了一些關于細節(jié)的低層次陳述。這樣的規(guī)格說明書使得讀者很難了解系統的整體功能結構。 4.1.2 形式化方法的優(yōu)點人在理解用自然語言描述的規(guī)格說明時，容易產生二義性。為了克服非形式化方法的缺點，人們把數學引入軟件開發(fā)過程，創(chuàng)造了基于數學的形式化方法。在開發(fā)大型軟件系統的過程中應用數學，能夠帶來下述的幾個優(yōu)點：數學最有用的一個性質是，它能夠簡潔準確地描述物理現象、對象或動作的結果，因此是理想的建模工具。數學特別適合于表示狀態(tài)，也就是表示“做什么”。 需求規(guī)格說明書主要描述應用系統在運行前和運行后的狀態(tài)，因此，數學比自然語言更適于描述詳細的需求。在理想情況下，分析員可以寫出系統的數學規(guī)格說明，它準確到幾乎沒有二義性，而且可以用數學方法來驗證，以發(fā)現存在的矛盾和不完整性，在這樣的規(guī)格說明中完全沒有含糊性。但是，實際情況并不這么簡單，軟件系統的復雜性是出了名的，希望用少數幾個數學公式來描述它，是根本不可能的。此外，即使應用了形式化方法，完整性也是難于保證的：由于溝通不夠，可能遺漏了客戶的一些需求；規(guī)格說明的撰寫者可能有意省略了系統的某些特征，以便設計者在選擇實現方法時有一定自由度；要設想出使用一個大型復雜系統的每一個可能的情景，通常是做不到的。 在軟件開發(fā)過程中使用數學的另一個優(yōu)點是，可以在不同的軟件工程活動之間平滑地過渡。不僅功能規(guī)格說明，而且系統設計也可以用數學表達，當然，程序代碼也是一種數學符號(雖然是一種相當繁瑣、冗長的數學符號)。數學作為軟件開發(fā)工具的最后一個優(yōu)點是，它提供了高層確認的手段�？梢允褂脭祵W方法證明，設計符合規(guī)格說明，程序代碼正確地實現了設計結果。 4.1.3 應用形式化方法的準則人們對形式化方法的看法并不一致。形式化方法對某些軟件工程師很有吸引力，其擁護者甚至宣稱這種方法可以引發(fā)軟件開發(fā)方法的革命；另一些人則對把數學引入軟件開發(fā)過程持懷疑甚至反對的態(tài)度。編者認為，對形式化方法也應該“一分為二”，既不要過分夸大它的優(yōu)點也不要一概排斥。為了更好地發(fā)揮這種方法的長處，下面給出應用形式化方法的幾條準則，供讀者在實際工作中使用。 (1) 應該選用適當的表示方法。通常，一種規(guī)格說明技術只能用自然的方式說明某一類概念，如果用這種技術描述其不適于描述的概念，則不僅工作量大而且描述方式也很復雜。因此，應該仔細選擇一種適用于當前項目的形式化說明技術。 (2) 應該形式化，但不要過分形式化。目前的形式化技術還不適于描述系統的每個方面。但是，也不能因此就認為完全沒必要采用形式化方法。形式化規(guī)格說明技術要求我們非常準確地描述事物，因此有助于防止含糊和誤解。事實上，如果用形式化方法仔細說明系統中易出錯的或關鍵的部分，則只用適中的工作量就能獲得較大回報。 (3) 應該估算成本。為了使用形式化方法，通常需要事先進行大量的培訓。最好預先估算所需的成本并編入預算。 (4) 應該有形式化方法顧問隨時提供咨詢。絕大多數軟件工程師對形式化方法中使用的數學和邏輯并不很熟悉，而且沒受過使用形式化方法的專業(yè)訓練，因此，需要專家指導和培訓。 (5) 不應該放棄傳統的開發(fā)方法。把形式化方法和結構化方法或面向對象方法集成起來是可能的，而且由于取長補短往往能獲得很好的效果。 (6) 應該建立詳盡的文檔。建議使用自然語言注釋形式化的規(guī)格說明書，以幫助用戶和維護人員理解系統。 (7) 不應該放棄質量標準。形式化方法并不能保證軟件的正確性，它們只不過是有助于開發(fā)出高質量軟件的一種手段。除了使用形式化說明技術外，在系統開發(fā)過程中仍然必須一如既往地實施其他質量保證活動。 (8) 不應該盲目依賴形式化方法。這種方法不是包治百病的靈丹妙藥，它們只不過是眾多工具中的一種。形式化方法并不能保證開發(fā)出的軟件絕對正確，例如，無法用形式化方法證明從非形式化需求到形式化規(guī)格說明的轉換是正確的，因此，必須用其他方法(例如，評審、測試)來驗證軟件正確性。 (9) 應該測試、測試再測試。形式化方法不僅不能保證軟件系統絕對正確，也不能證明系統性能或其他質量指標符合需要，因此，軟件測試的重要性并沒有降低。 (10) 應該重用。即使采用了形式化方法，軟件重用仍然是降低軟件成本和提高軟件質量的惟一合理的方法。而且用形式化方法說明的軟件構件具有清晰定義的功能和接口，使得它們有更好的可重用性。 4.2 有窮狀態(tài)機 4.2.1 概念下面通過一個簡單例子介紹有窮狀態(tài)機的基本概念。一個保險箱上裝了一個復合鎖，鎖有三個位置，分別標記為1、2、3，轉盤可向左(L)或向右(R)轉動。這樣，在任意時刻轉盤都有6種可能的運動，即1L、1R、2L、2R、3L和3R。保險箱的組合密碼是1L、3R、2L，轉盤的任何其他運動都將引起報警。圖4.1描繪了保險箱的狀態(tài)轉換情況。 圖4.1 保險箱的狀態(tài)轉換圖 圖4.1是一個有窮狀態(tài)機的狀態(tài)轉換圖。狀態(tài)轉換并不一定要用圖形方式描述，表4.1（見書68頁）的表格形式也可以表達同樣的信息。從上面這個簡單例子可以看出，一個有窮狀態(tài)機包括下述5個部分：狀態(tài)集J、輸入集K、由當前狀態(tài)和當前輸入確定下一個狀態(tài)(次態(tài))的轉換函數T、初始態(tài)S和終態(tài)集F。對于保險箱的例子，相應的有窮狀態(tài)機的各部分如下。狀態(tài)集J：｛保險箱鎖定，A，B，保險箱解鎖，報警｝。輸入集K：｛1L，1R，2L，2R，3L，3R｝。 轉換函數T：如表4.1所示。初始態(tài)S：保險箱鎖定。終態(tài)集F：｛保險箱解鎖，報警｝。如果使用更形式化的術語，一個有窮狀態(tài)機可以表示為一個5元組(J，K，T，S，F)，其中： J是一個有窮的非空狀態(tài)集； K是一個有窮的非空輸入集； T是一個從(J-F)×K到J的轉換函數； S∈J，是一個初始狀態(tài)； F?J，是終態(tài)集。 有窮狀態(tài)機的概念在計算機系統中應用得非常廣泛。例如，每個菜單驅動的用戶界面都是一個有窮狀態(tài)機的實現。一個菜單的顯示和一個狀態(tài)相對應，鍵盤輸入或用鼠標選擇一個圖標是使系統進入其他狀態(tài)的一個事件。狀態(tài)的每個轉換都具有下面的形式：當前狀態(tài)〔菜單〕+事件〔所選擇的項〕?下個狀態(tài)。 為了對一個系統進行規(guī)格說明，通常都需要對有窮狀態(tài)機做一個很有用的擴展，即在前述的5元組中加入第6個組件——謂詞集P，從而把有窮狀態(tài)機擴展為一個6元組，其中每個謂詞都是系統全局狀態(tài)Y的函數。轉換函數T現在是一個從(J-F)×K×P到J的函數�，F在的轉換規(guī)則形式如下：當前狀態(tài)〔菜單〕+事件〔所選擇的項〕+謂詞?下個狀態(tài)。 4.2.2 例子為了具體說明怎樣用有窮狀態(tài)機技術表達系統的規(guī)格說明，現在用這種技術給出大家熟悉的電梯系統的規(guī)格說明。首先給出用自然語言描述的對電梯系統的需求：在一幢m層的大廈中需要一套控制n部電梯的產品，要求這n部電梯按照約束條件C1，C2和C3在樓層間移動。 C1：每部電梯內有m個按鈕，每個按鈕代表一個樓層。當按下一個按鈕時該按鈕指示燈亮，同時電梯駛向相應的樓層，到達按鈕指定的樓層時指示燈熄滅。 C2：除了大廈的最低層和最高層之外，每層樓都有兩個按鈕分別請求電梯上行和下行。這兩個按鈕之一被按下時相應的指示燈亮，當電梯到達此樓層時燈熄滅，電梯向要求的方向移動。 C3：當對電梯沒有請求時，它關門并停在當前樓層�，F在使用一個擴展的有窮狀態(tài)機對本產品進行規(guī)格說明。這個問題中有兩個按鈕集。n部電梯中的每一部都有m個按鈕，一個按鈕對應一個樓層。因為這m×n個按鈕都在電梯中，所以稱它們?yōu)殡娞莅粹o。此外，每層樓有兩個按鈕，一個請求向上，另一個請求向下，這些按鈕稱為樓層按鈕。 電梯按鈕的狀態(tài)轉換圖如圖4.2所示。令EB(e，f)表示按下電梯e內的按鈕并請求到f層去。EB(e，f)有兩個狀態(tài)，分別是按鈕發(fā)光(打開)和不發(fā)光(關閉)。更精確地說，狀態(tài)是： EBON(e，f)：電梯按鈕(e，f)打開 EBOFF(e，f)：電梯按鈕(e，f)關閉如果電梯按鈕(e，f)發(fā)光且電梯到達f層，該按鈕將熄滅。相反如果按鈕熄滅，則按下它時，按鈕將發(fā)光。上述描述中包含了兩個事件，它們分別是： EBP(e，f)：電梯按鈕(e，f)被按下 EAF(e，f)：電梯e到達f層 圖4.2 電梯按鈕的狀態(tài)轉換圖 圖4.3樓層按鈕的狀態(tài)轉換圖 為了定義與這些事件和狀態(tài)相聯系的狀態(tài)轉換規(guī)則，需要一個謂詞V(e，f)，它的含義如下： V(e，f)：電梯e停在f層如果電梯按鈕(e，f)處于關閉狀態(tài)〔當前狀態(tài)〕，而且電梯按鈕(e，f)被按下〔事件〕，而且電梯e不在f層〔謂詞〕，則該電梯按鈕打開發(fā)光〔下個狀態(tài)〕。狀態(tài)轉換規(guī)則的形式化描述如下： EBOFF(e，f)+EBP(e，f)+not V(e，f)?EBON(e，f) 反之，如果電梯到達f層，而且電梯按鈕是打開的，于是它就會熄滅。這條轉換規(guī)則可以形式化地表示為： EBON(e，f)+EAF(e，f)?EBOFF(e，f) 接下來考慮樓層按鈕。令FB(d，f)表示f層請求電梯向d方向運動的按鈕，樓層按鈕FB(d，f)的狀態(tài)轉換圖如圖4.3所示。樓層按鈕的狀態(tài)如下： FBON(d，f)：樓層按鈕(d，f)打開 FBOFF(d，f)：樓層按鈕(d，f)關閉如果樓層按鈕已經打開，而且一部電梯到達f層，則按鈕關閉。反之，如果樓層按鈕原來是關閉的，被按下后該按鈕將打開。這段敘述中包含了以下兩個事件。 FBP(d，f)：樓層按鈕(d，f)被按下 EAF(1…n，f)：電梯1或…或n到達f層其中1…n表示或為1或為2…或為n。為了定義與這些事件和狀態(tài)相聯系的狀態(tài)轉換規(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)，形式化轉換規(guī)則為： FBOFF(d，f)+FBP(d，f)+not S(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方向運動的樓層按鈕處于關閉狀態(tài)，現在該按鈕被按下，并且當時沒有正停在f層準備向d方向移動的電梯，則該樓層按鈕打開。反之，如果樓層按鈕已經打開，且至少有一部電梯到達f層，該部電梯將朝d方向運動，則按鈕將關閉。 在討論電梯按鈕狀態(tài)轉換規(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) 定義電梯按鈕和樓層按鈕的狀態(tài)都是很簡單、直觀的事情�，F在轉向討論電梯的狀態(tài)及其轉換規(guī)則，就會出現一些復雜的情況。一個電梯狀態(tài)實質上包含許多子狀態(tài)。下面定義電梯的3個狀態(tài)： M(d，e，f)：電梯e正沿d方向移動，即將到達的是第f層 S(d，e，f)：電梯e停在f層，將朝d方向移動(尚未關門) W(e，f)：電梯e在f層等待(已關門) 其中S(d，e，f)狀態(tài)已在討論樓層按鈕時定義過，但是，現在的定義更完備一些。圖4.4是電梯的狀態(tài)轉換圖。3個電梯停止狀態(tài)S(U，e，f)、S(N，e，f)和S(D，e，f)已被組合成一個大的狀態(tài)，這樣做的目的是減少狀態(tài)總數以簡化流圖。圖4.4中包含了下述3個可觸發(fā)狀態(tài)發(fā)生改變的事件。 DC(e，f)：電梯e在樓層f關上門 ST(e，f)：電梯e靠近f層時觸發(fā)傳感器，電梯控制器決定在當前樓層電梯是否停下 RL：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)，登錄需求 圖4.4 電梯的狀態(tài)轉換圖 最后，給出電梯的狀態(tài)轉換規(guī)則。為簡單起見，這里給出的規(guī)則僅發(fā)生在關門之時。 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層準備向上移動，且門已經關閉，則電梯將向上一樓層移動。第二條和第三條規(guī)則，分別對應于電梯即將下降或者沒有待處理的請求的情況。 4.2.3 評價有窮狀態(tài)機方法采用了一種簡單的格式來描述規(guī)格說明：當前狀態(tài)+事件+謂詞?下個狀態(tài)這種形式的規(guī)格說明易于書寫、易于驗證，而且可以比較容易地把它轉變成設計或程序代碼。事實上，可以開發(fā)一個CASE工具把一個有窮狀態(tài)機規(guī)格說明直接轉變?yōu)樵创�碼。維護可以通過重新轉變來實現，也就是說，如果需要一個新的狀態(tài)或事件，首先修改規(guī)格說明，然后直接由新的規(guī)格說明生成新版本的產品。 有窮狀態(tài)機方法比數據流圖技術更精確，而且和它一樣易于理解。不過，它也有缺點：在開發(fā)一個大系統時三元組(即狀態(tài)、事件、謂詞)的數量會迅速增長。此外，和數據流圖方法一樣，形式化的有窮狀態(tài)機方法也沒有處理定時需求。下節(jié)將介紹的Petri網技術，是一種可處理定時問題的形式化方法。 4.3 Petri網 4.3.1 概念并發(fā)系統中遇到的一個主要問題是定時問題。這個問題可以表現為多種形式，如同步問題、競爭條件以及死鎖問題。定時問題通常是由不好的設計或有錯誤的實現引起的，而這樣的設計或實現通常又是由不好的規(guī)格說明造成的。如果規(guī)格說明不恰當，則有導致不完善的設計或實現的危險。用于確定系統中隱含的定時問題的一種有效技術是Petri網，這種技術的一個很大的優(yōu)點是它也可以用于設計中。 etri網是由Carl Adam Petri發(fā)明的。最初只有自動化專家對Petri網感興趣，后來Petri網在計算機科學中也得到廣泛的應用，例如，在性能評價、操作系統和軟件工程等領域，Petri網應用得都比較廣泛。特別是已經證明，用Petri網可以有效地描述并發(fā)活動。 Petri網包含4種元素：一組位置P、一組轉換T、輸入函數I以及輸出函數O。圖4.5舉例說明了Petri網的組成。 圖4.5 Petri網的組成 一組位置P為｛P1，P2，P3，P4｝，在圖中用圓圈代表位置。一組轉換T為｛t1，t2｝，在圖中用短直線表示轉換。兩個用于轉換的輸入函數，用由位置指向轉換的箭頭表示，它們是： I(t1)=｛P2，P4｝ I(t2)=｛P2｝兩個用于轉換的輸出函數，用由轉換指向位置的箭頭表示，它們是： O(t1)=｛P1｝ O(t2)=｛P3，P3｝ 注意，輸出函數O(t2)中有兩個P3，是因為有兩個箭頭由t2指向P3。更形式化的Petri網結構，是一個四元組C=(P，T，I，O)。其中， P=｛P1，…，Pn｝是一個有窮位置集，n≥0。 T=｛t1，…，tm｝是一個有窮轉換集，m≥0，且T和P不相交。 I：T→P∞為輸入函數，是由轉換到位置無序單位組(bags)的映射。 O：T→P∞為輸出函數，是由轉換到位置無序單位組的映射。 一個無序單位組或多重組是允許一個元素有多個實例的廣義集。 Petri網的標記是在Petri網中權標(token)的分配。例如，在圖4.6中有4個權標，其中一個在P1中，兩個在P2中，P3中沒有，還有一個在P4中。上述標記可以用向量(1，2，0，1)表示。由于P2和P4中有權標，因此t1啟動(即被激發(fā))。通常，當每個輸入位置所擁有的權標數大于等于從該位置到轉換的線數時，就允許轉換。當t1被激發(fā)時，P2和P4上各有一個權標被移出，而P1上則增加一個權標。Petri網中權標總數不是固定的，在這個例子中兩個權標被移出，而P1上只能增加一個權標。 在圖4.6中P2上有權標，因此t2也可以被激發(fā)。當t2被激發(fā)時，P2上將移走一個權標，而P3上新增加兩個權標。Petri網具有非確定性，也就是說，如果數個轉換都達到了激發(fā)條件，則其中任意一個都可以被激發(fā)。圖4.6所示Petri網的標記為(1，2，0，1)，t1和t2都可以被激發(fā)。假設t1被激發(fā)了，則結果如圖4.7所示，標記為(2，1，0，0)。此時，只有t2可以被激發(fā)。如果t2也被激發(fā)了，則權標從P2中移出，兩個新權標被放在P3上，結果如圖4.8所示，標記為(2，0，2，0)。 圖4.6 帶標記的Petri網 圖4.7 圖4.6的Petri網在轉換 t1被激發(fā)后的情況 圖4.8 圖4.7的Petri網在轉換 t2被激發(fā)后的情況 圖4.9 含禁止線的Petri網 更形式化地說，Petri網C=(P，T，I，O)中的標記M，是由一組位置P到一組非負整數的映射： M：P→｛0，1，2，…｝這樣，帶有標記的Petri網成為一個五元組(P，T，I，O，M)。對Petri網的一個重要擴充是加入禁止線。如圖4.9所示，禁止線是用一個小圓圈而不是用箭頭標記的輸入線。通常，當每個輸入線上至少有一個權標，而禁止線上沒有權標的時候，相應的轉換才是允許的。在圖4.9中，P3上有一個權標而P2上沒有權標，因此轉換t1可以被激發(fā)。 4.3.2 例子現在把Petri網應用于上一節(jié)討論過的電梯問題。當用Petri網表示電梯系統的規(guī)格說明時，每個樓層用一個位置Ff代表(1≤f≤m)，在Petri網中電梯是用一個權標代表的。在位置Ff上有權標，表示在樓層f上有電梯。 1. 電梯按鈕電梯問題的第一個約束條件描述了電梯按鈕的行為，現在復述一下這個約束條件。 第一條約束C1：每部電梯有m個按鈕，每層對應一個按鈕。當按下一個按鈕時該按鈕指示燈亮，指示電梯移往相應的樓層。當電梯到達指定的樓層時，按鈕將熄滅。為了用Petri網表達電梯按鈕的規(guī)格說明，在Petri網中還必須設置其他的位置。電梯中樓層f的按鈕，在Petri網中用位置EBf表示(1≤f≤m)。在EBf上有一個權標，就表示電梯內樓層f的按鈕被按下了。 電梯按鈕只有在第一次被按下時才會由暗變亮，以后再按它則只會被忽略。圖4.10所示的Petri網準確地描述了電梯按鈕的行為規(guī)律。首先，假設按鈕沒有發(fā)亮，顯然在位置EBf上沒有權標，從而在存在禁止線的情況下，轉換“EBf被按下”是允許發(fā)生的。假設現在按下按鈕，則轉換被激發(fā)并在EBf上放置了一個權標，如圖4.10所示。以后不論再按下多少次按鈕，禁止線與現有權標的組合都決定了轉換“EBf被按下”不能再被激發(fā)了，因此，位置EBf上的權標數不會多于1。 圖4.10 Petri網表示的電梯按鈕 假設電梯由g層駛向f層，因為電梯在g層，如圖4.10所示，位置Fg上有一個權標。由于每條輸入線上各有一個權標，轉換“電梯在運行”被激發(fā)，從而EBf和Fg上的權標被移走，按鈕EBf被關閉，在位置Ff上出現一個新權標，即轉換的激發(fā)使電梯由g層駛到f層。事實上，電梯由g層移到f層是需要時間的，為處理這個情況及其他類似的問題(例如，由于物理上的原因按鈕被按下后不能馬上發(fā)亮)，Petri網模型中必須加入時限。也就是說，在標準Petri網中轉換是瞬時完成的，而在現實情況下就需要時間控制Petri網，以使轉換與非零時間相聯系。 2. 樓層按鈕在第二個約束條件中描述了樓層按鈕的行為。第二條約束C2：除了第一層與頂層之外，每個樓層都有兩個按鈕，一個要求電梯上行，另一個要求電梯下行。這些按鈕在按下時發(fā)亮，當電梯到達該層并將向指定方向移動時，相應的按鈕才會熄滅。在Petri網中樓層按鈕用位置FBfu和FBfd表示，分別代表f樓層請求電梯上行和下行的按鈕。底層的按鈕為FB1u，最高層的按鈕為FBmd，中間每一層有兩個按鈕FBfu和FBfd(1＜f＜m)。 圖4.11 Petri網表示樓層按鈕 圖4.11所示的情況為電梯由g層駛向f層。根據電梯乘客的要求，某一個樓層按鈕亮或兩個樓層按鈕都亮。如果兩個按鈕都亮了，則只有一個按鈕熄滅。圖4.11所示的Petri網可以保證，當兩個按鈕都亮了的時候，只有一個按鈕熄滅。但是要保證按鈕熄滅正確，則需要更復雜的Petri網模型。最后，考慮第三條約束。第三條約束C3：當電梯沒有收到請求時，它將停留在當前樓層并關門。這條約束很容易實現，如圖4.11所示，當沒有請求(FBfu和FBfd上無權標）時，任何一個轉換“電梯在運行”都不能被激發(fā)。 4.4 Z語言 4.4.1 簡介用Z語言描述的、最簡單的形式化規(guī)格說明含有下述4個部分：給定的集合、數據類型及常數。狀態(tài)定義。初始狀態(tài)。操作。 1. 給定的集合一個Z規(guī)格說明從一系列給定的初始化集合開始。所謂初始化集合就是不需要詳細定義的集合，這種集合用帶方括號的形式表示。對于電梯問題，給定的初始化集合稱為Button，即所有按鈕的集合，因此，Z規(guī)格說明開始于：〔Button〕 2. 狀態(tài)定義一個Z規(guī)格說明由若干個“格(schema)”組成，每個格含有一組變量說明和一系列限定變量取值范圍的謂詞。例如，格S的格式如圖4.12所示。 圖4.12 Z格S的格式 在電梯問題中，Button有4個子集，即floor_buttons(樓層按鈕的集合)、elevator_buttons(電梯按鈕的集合)、buttons(電梯問題中所有按鈕的集合)以及pushed(所有被按的按鈕的集合，即所有處于打開狀態(tài)的按鈕的集合)。圖4.13（見書76頁）描述了格Button_State，其中，符號P表示冪集(即給定集的所有子集)。約束條件聲明，floor_buttons集與elevator_buttons集不相交，而且它們共同組成buttons集(在下面的討論中并不需要floor_buttons集和elevator_buttons集，把它們放于圖4.13中只是用來說明Z格包含的內容)。 3. 初始狀態(tài)抽象的初始狀態(tài)是指系統第一次開啟時的狀態(tài)。對于電梯問題來說，抽象的初始狀態(tài)為： Button_Init?〔Button_State｜pushed=Φ〕上式表示，當系統首次開啟時pushed集為空，即所有按鈕都處于關閉狀態(tài)。 4. 操作如果一個原來處于關閉狀態(tài)的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到pushed集中。圖4.14（見書77頁）定義了操作Push_Button(按按鈕)。 操作的謂詞部分，包含了一組調用操作的前置條件，以及操作完全結束后的后置條件。如果前置條件成立，則操作執(zhí)行完成后可得到后置條件。但是，如果在前置條件不成立的情況下調用該操作，則不能得到指定的結果(因此結果無法預測)。假設電梯到達了某樓層，如果相應的樓層按鈕已經打開，則此時它會關閉；同樣，如果相應的電梯按鈕已經打開，則此時它也會關閉。也就是說，如果“button?”屬于pushed集，則將它移出該集合，如圖4.15（見書77頁）所示(符號“＼”表示集合差運算)。 4.4.2 評價已經在許多軟件開發(fā)項目中成功地運用了Z語言，目前，Z也許是應用得最廣泛的形式化語言，尤其是在大型項目中Z語言的優(yōu)勢更加明顯。Z語言之所以會獲得如此多的成功，主要有以下幾個原因： (1) 可以比較容易地發(fā)現用Z寫的規(guī)格說明的錯誤，特別是在自己審查規(guī)格說明，及根據形式化的規(guī)格說明來審查設計與代碼時，情況更是如此。 (2) 用Z寫規(guī)格說明時，要求作者十分精確地使用Z說明符。由于對精確性的要求很高，從而和非形式化規(guī)格說明相比，減少了模糊性、不一致性和遺漏。 (3) Z是一種形式化語言，在需要時開發(fā)者可以嚴格地驗證規(guī)格說明的正確性。 (4) 雖然完全學會Z語言相當困難，但是，經驗表明，只學過中學數學的軟件開發(fā)人員仍然可以只用比較短的時間就學會編寫Z規(guī)格說明，當然，這些人還沒有能力證明規(guī)格說明的結果是否正確。 (5) 使用Z語言可以降低軟件開發(fā)費用。雖然用Z寫規(guī)格說明所需用的時間比使用非形式化技術要多，但開發(fā)過程所需要的總時間卻減少了。 (6) 雖然用戶無法理解用Z寫的規(guī)格說明，但是，可以依據Z規(guī)格說明用自然語言重寫規(guī)格說明。經驗證明，這樣得到的自然語言規(guī)格說明，比直接用自然語言寫出的非形式化規(guī)格說明更清楚、更正確。使用形式化規(guī)格說明是全球的總趨勢，過去，主要是歐洲習慣于使用形式化規(guī)格說明技術，現在越來越多的美國公司也開始使用形式化規(guī)格說明技術。 4.5 小結基于數學的形式化規(guī)格說明技術，目前還沒有在軟件產業(yè)界廣泛應用，但是，與欠形式化的方法比較起來，它確實有實質性的優(yōu)點：形式化的規(guī)格說明可以用數學方法研究、驗證(例如，一個正確的程序可以被證明滿足其規(guī)格說明，兩個規(guī)格說明可以被證明是等價的，規(guī)格說明中存在的某些形式的不完整性和不一致性可以被自動地檢測出來)。此外，形式化的規(guī)格說明消除了二義性，而且它鼓勵軟件開發(fā)者在軟件工程過程的早期階段使用更嚴格的方法，從而可以減少差錯。 當然，形式化方法也有缺點：大多數形式化的規(guī)格說明主要關注于系統的功能和數據，而問題的時序、控制和行為等方面的需求卻更難于表示。此外，形式化方法比欠形式化方法更難學習，不僅在培訓階段要花大量的投資，而且對某些軟件工程師來說，它代表了一種“文化沖擊”。把形式化方法和欠形式化方法有機地結合起來，使它們取長補短，應該能獲得更理想的效果。本章講述的應用形式化方法的準則(見4.1.3節(jié))，對于讀者今后在實際工作中更好地利用形式化方法，可能是有幫助的。習題 4-1 舉例對比形式化方法和欠形式化方法的優(yōu)缺點。 4-2 在什么情況下應該使用形式化說明技術?使用形式化說明技術時應遵守哪些準則? 4-3 一個浮點二進制數的構成是：一個可選的符號(+或-)，后跟一個或多個二進制位，再跟上一個字符E，再加上另一個可選符號(+或-)及一個或多個二進制位。例如，下列的字符串都是浮點二進制數： 110101E-101 -100111E11101 +1E0 更形式化地，浮點二進制數定義如下：〈floating?point binary〉∷=［〈sign〉］〈bitstring〉E［〈sign〉］〈bitstring〉〈sign〉∷=+｜- 〈bitstring〉∷=〈bit〉［〈bitstring〉］〈bit〉∷=0｜1 其中，符號∷=表示定義為；符號［...］表示可選項； 符號a｜b表示a或b。假設有這樣一個有窮狀態(tài)機：以一串字符為輸入，判斷字符串中是否含有合法的浮點二進制數。試對這個有窮狀態(tài)機進行規(guī)格說明。 4-4 考慮下述的自動化圖書館流通系統：每本書都有一個條形碼，每個借閱人都有一個帶有條形碼的卡片。當一個借閱人想借一本書時，圖書管理員掃描書上的條形碼和借閱人卡片上的條形碼，然后在計算機終端上輸入C；當歸還一本書時，圖書管理員將再做一次掃描，并輸入R。圖書管理員可以把一些書加到(+)圖書集合中，也可以刪除(-)它們。 借閱人可以在終端上查找到某個作者所有的書(輸入“A=”和作者名字)，或具有指定標題的所有書籍(輸入“T=”和標題)，或屬于特定主題范圍內的所有圖書(輸入“S=”加主題范圍)。最后，如果借閱人想借的書已被別人借走，圖書管理員將給這本書設置一個預約，以便書歸還時把書留給預約的借閱人(輸入“H=”加書號)。試用有窮狀態(tài)機說明上述的圖書流通系統。 4-5 試用Petri網說明第4題所述圖書館中一本書的循環(huán)過程。在規(guī)格說明中應該包括操作H、C及R。 4-6 試用Z語言對第4題所述圖書館圖書流通系統做一個完整的規(guī)格說明。WX2紅軟基地

軟件工程基礎ppt：這是軟件工程基礎ppt，包括了軟件需求分析與定義，可行性研究，可行性研究工作步驟，軟件設計，軟件測試，軟件維護，軟件維護的分類，軟件過程管理，類圖等內容，歡迎點擊下載。

實用軟件工程ppt：這是實用軟件工程ppt，包括了軟件工程概述，軟件工程的概念，發(fā)展歷程，軟件工程的生命周期，建模的目的等內容，歡迎點擊下載。

軟件工程類答辯ppt：這是軟件工程類答辯ppt，包括了系統介紹，研究背景，需求分析，系統設計，系統實現，總結，致謝等內容，歡迎點擊下載。