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

軟件工程導(dǎo)論ppt是由紅軟PPT免費(fèi)下載網(wǎng)推薦的一款學(xué)校PPT類型的PowerPoint.

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

軟件工程基礎(chǔ)ppt：這是軟件工程基礎(chǔ)ppt，包括了軟件需求分析與定義，可行性研究，可行性研究工作步驟，軟件設(shè)計(jì)，軟件測(cè)試，軟件維護(hù)，軟件維護(hù)的分類，軟件過程管理，類圖等內(nèi)容，歡迎點(diǎn)擊下載。

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

軟件工程類答辯ppt：這是軟件工程類答辯ppt，包括了系統(tǒng)介紹，研究背景，需求分析，系統(tǒng)設(shè)計(jì)，系統(tǒng)實(shí)現(xiàn)，總結(jié)，致謝等內(nèi)容，歡迎點(diǎn)擊下載。