軟件工程課件之第4章_形式化說明技術(shù)(第五版)(張海潘編著)

1、4.1 概述概述4.2 有窮狀態(tài)機有窮狀態(tài)機4.3 Petri網(wǎng)網(wǎng)4.4 Z語言語言第第4章章 形式化說明技術(shù)形式化說明技術(shù)軟件工程使用方法的分類：軟件工程使用方法的分類：n非形式化，用自然語言描述需求規(guī)格說明；非形式化，用自然語言描述需求規(guī)格說明；n半形式化，用數(shù)據(jù)流圖或?qū)嶓w半形式化，用數(shù)據(jù)流圖或?qū)嶓w-聯(lián)系圖建立模聯(lián)系圖建立模型；型；n形式化，是描述系統(tǒng)性質(zhì)的基于數(shù)學的技術(shù)，形式化，是描述系統(tǒng)性質(zhì)的基于數(shù)學的技術(shù)，也就是說，如果一種方法有堅實的數(shù)學基礎(chǔ)，也就是說，如果一種方法有堅實的數(shù)學基礎(chǔ)，那么它就是形式化的。那么它就是形式化的。 4.1 概述概述4.1.1 非形式化方法的缺點非形式化方法

2、的缺點n矛盾，指一組相互沖突的陳述。矛盾，指一組相互沖突的陳述。n二義性，指讀者可以用不同方式理解的陳述。二義性，指讀者可以用不同方式理解的陳述。n含糊性，幾乎不可避免地會出現(xiàn)含糊性。含糊性，幾乎不可避免地會出現(xiàn)含糊性。n不完整性，不完整性可能是在系統(tǒng)規(guī)格說明不完整性，不完整性可能是在系統(tǒng)規(guī)格說明中最常遇到的問題之一。中最常遇到的問題之一。n抽象層次混亂，指在非常抽象的陳述中混進抽象層次混亂，指在非常抽象的陳述中混進了一些關(guān)于細節(jié)的低層次陳述。了一些關(guān)于細節(jié)的低層次陳述。 4.1.2 形式化方法的優(yōu)點形式化方法的優(yōu)點n數(shù)學能夠簡潔準確地描述物理現(xiàn)象、對象或動數(shù)學能夠簡潔準確地描述物理現(xiàn)象、對象

3、或動作的結(jié)果，因此是理想的建模工具。特別適合作的結(jié)果，因此是理想的建模工具。特別適合于表示狀態(tài)，也就是表示于表示狀態(tài)，也就是表示“做什么做什么”。n可以在不同的軟件工程活動之間平滑地過渡?？梢栽诓煌能浖こ袒顒又g平滑地過渡。不僅功能規(guī)格說明，而且系統(tǒng)設(shè)計也可以用數(shù)不僅功能規(guī)格說明，而且系統(tǒng)設(shè)計也可以用數(shù)學表達，當然，程序代碼也是一種數(shù)學符號。學表達，當然，程序代碼也是一種數(shù)學符號。n它提供了高層確認的手段?？梢允褂脭?shù)學方法它提供了高層確認的手段?？梢允褂脭?shù)學方法證明，設(shè)計符合規(guī)格說明，程序代碼正確地實證明，設(shè)計符合規(guī)格說明，程序代碼正確地實現(xiàn)了設(shè)計結(jié)果?，F(xiàn)了設(shè)計結(jié)果。 4.1.3 應(yīng)用形式

4、化方法的準則應(yīng)用形式化方法的準則(1) 應(yīng)該選用適當?shù)谋硎痉椒☉?yīng)該選用適當?shù)谋硎痉椒?通常，一種規(guī)格說明技術(shù)只能用自然的方通常，一種規(guī)格說明技術(shù)只能用自然的方式說明某一類概念。式說明某一類概念。(2) 應(yīng)該形式化，但不要過分形式化應(yīng)該形式化，但不要過分形式化 目前的形式化技術(shù)還不適于描述系統(tǒng)的每目前的形式化技術(shù)還不適于描述系統(tǒng)的每個方面。個方面。(3) 應(yīng)該估算成本應(yīng)該估算成本 為了使用形式化方法，通常需要事先進行為了使用形式化方法，通常需要事先進行大量的培訓(xùn)。最好預(yù)先估算所需的成本并編入大量的培訓(xùn)。最好預(yù)先估算所需的成本并編入預(yù)算。預(yù)算。(4) 應(yīng)該有形式化方法顧問隨時提供咨詢應(yīng)該有形式化方

5、法顧問隨時提供咨詢 絕大多數(shù)軟件工程師對形式化方法中使用絕大多數(shù)軟件工程師對形式化方法中使用的數(shù)學和邏輯并不很熟悉，沒受過使用形式化的數(shù)學和邏輯并不很熟悉，沒受過使用形式化方法的專業(yè)訓(xùn)練，因此需要專家指導(dǎo)和培訓(xùn)。方法的專業(yè)訓(xùn)練，因此需要專家指導(dǎo)和培訓(xùn)。(5) 不應(yīng)該放棄傳統(tǒng)的開發(fā)方法不應(yīng)該放棄傳統(tǒng)的開發(fā)方法 把形式化方法和結(jié)構(gòu)化方法或面向?qū)ο蠓桨研问交椒ê徒Y(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋砣￠L補短往往能獲得很好的效果。法集成起來取長補短往往能獲得很好的效果。 (6) 應(yīng)該建立詳盡的文檔應(yīng)該建立詳盡的文檔 建議使用自然語言注釋形式化的規(guī)格說明建議使用自然語言注釋形式化的規(guī)格說明書，以幫助用戶和維

6、護人員理解系統(tǒng)。書，以幫助用戶和維護人員理解系統(tǒng)。 (7) 不應(yīng)該放棄質(zhì)量標準不應(yīng)該放棄質(zhì)量標準 形式化方法不能保證軟件的正確性，只不形式化方法不能保證軟件的正確性，只不過是有助于開發(fā)出高質(zhì)量軟件的一種手段。過是有助于開發(fā)出高質(zhì)量軟件的一種手段。 (8) 不應(yīng)該盲目依賴形式化方法不應(yīng)該盲目依賴形式化方法 形式化方法并不能保證開發(fā)出的軟件絕對形式化方法并不能保證開發(fā)出的軟件絕對正確，必須用其他方法來驗證軟件正確性。正確，必須用其他方法來驗證軟件正確性。(9) 應(yīng)該測試、測試再測試應(yīng)該測試、測試再測試 軟件測試的重要性并沒有降低。軟件測試的重要性并沒有降低。(10) 應(yīng)該重用應(yīng)該重用 軟件重用仍然

7、是降低軟件成本和提高軟件軟件重用仍然是降低軟件成本和提高軟件質(zhì)量的惟一合理的方法。質(zhì)量的惟一合理的方法。4.2 有窮狀態(tài)機有窮狀態(tài)機4.2.1 概念概念 例：例： 一個保險箱上裝了一個復(fù)合鎖，鎖有三一個保險箱上裝了一個復(fù)合鎖，鎖有三個位置，分別標記為個位置，分別標記為1、2、3，轉(zhuǎn)盤可向左，轉(zhuǎn)盤可向左(L)或向右或向右(R)轉(zhuǎn)動。這樣，在任意時刻轉(zhuǎn)盤都有轉(zhuǎn)動。這樣，在任意時刻轉(zhuǎn)盤都有6種可能的運動，即種可能的運動，即1L、1R、2L、2R、3L和和3R。保險箱的組合密碼是。保險箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤，轉(zhuǎn)盤的任何其他運動都將引起報警。的任何其他運動都將引起報警。 有窮狀態(tài)機包括有窮

8、狀態(tài)機包括5個部分：個部分：狀態(tài)集狀態(tài)集J、輸入集輸入集K、由當前狀態(tài)和當前輸入確定下一個狀態(tài)由當前狀態(tài)和當前輸入確定下一個狀態(tài)(次態(tài)次態(tài))的的轉(zhuǎn)換函數(shù)轉(zhuǎn)換函數(shù)T、初始態(tài)初始態(tài)S和和終態(tài)集終態(tài)集F。n狀態(tài)集狀態(tài)集J：保險箱鎖定，：保險箱鎖定，A，B，保險箱解鎖，保險箱解鎖，報警報警n輸入集輸入集K：1L，1R，2L，2R，3L，3Rn轉(zhuǎn)換函數(shù)轉(zhuǎn)換函數(shù)T：如表：如表4.1所示所示n初始態(tài)初始態(tài)S：保險箱鎖定：保險箱鎖定n終態(tài)集終態(tài)集F：保險箱解鎖，報警：保險箱解鎖，報警表表 4 4 . .1 1 保險箱的狀態(tài)轉(zhuǎn)換表保險箱的狀態(tài)轉(zhuǎn)換表當前狀態(tài)當前狀態(tài) 次態(tài)次態(tài)轉(zhuǎn)盤動作轉(zhuǎn)盤動作保險箱鎖定保險箱鎖定A

9、 AB B1L1LA A報警報警報警報警1R1R報警報警報警報警報警報警2L2L報警報警報警報警保險箱解鎖保險箱解鎖2R2R報警報警報警報警報警報警3L3L報警報警報警報警報警報警3R3R報警報警B B報警報警4.2.3 評價評價優(yōu)點：優(yōu)點：n形式簡單，易于書寫、易于驗證，比較容易地形式簡單，易于書寫、易于驗證，比較容易地把它轉(zhuǎn)變成設(shè)計或程序代碼。把它轉(zhuǎn)變成設(shè)計或程序代碼。n比數(shù)據(jù)流圖技術(shù)更精確，而且和它一樣易于理比數(shù)據(jù)流圖技術(shù)更精確，而且和它一樣易于理解。解。缺點：缺點：n在開發(fā)一個大系統(tǒng)時三元組在開發(fā)一個大系統(tǒng)時三元組(即狀態(tài)、事件、即狀態(tài)、事件、謂詞謂詞)的數(shù)量會迅速增長。的數(shù)量會迅速增

10、長。n和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機方和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機方法也沒有處理定時需求。法也沒有處理定時需求。 4.3 Petri網(wǎng)網(wǎng)4.3.1 概念概念 并發(fā)系統(tǒng)中遇到的一個主要問題是定時問并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題。這個問題可以表現(xiàn)為多種形式，如同步問題。這個問題可以表現(xiàn)為多種形式，如同步問題、競爭條件以及死鎖問題。如果規(guī)格說明不題、競爭條件以及死鎖問題。如果規(guī)格說明不恰當，則有導(dǎo)致不完善的設(shè)計或?qū)崿F(xiàn)的危險。恰當，則有導(dǎo)致不完善的設(shè)計或?qū)崿F(xiàn)的危險。用于確定系統(tǒng)中隱含的定時問題的一種有效技用于確定系統(tǒng)中隱含的定時問題的一種有效技術(shù)是術(shù)是Petri網(wǎng)，這種技術(shù)的

11、一個很大的優(yōu)點是網(wǎng)，這種技術(shù)的一個很大的優(yōu)點是它也可以用于設(shè)計中。它也可以用于設(shè)計中。 Petri網(wǎng)結(jié)構(gòu)，是一個四元組網(wǎng)結(jié)構(gòu)，是一個四元組C=(P,T,I,O)。其中。其中nP=P1,Pn是一個有窮位置集，是一個有窮位置集，n0。nT=t1,tm是一個有窮轉(zhuǎn)換集，是一個有窮轉(zhuǎn)換集，m0，且，且T和和P不相交。不相交。nI：TP為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組位組(bags)的映射。的映射。nO：TP為輸出函數(shù)，是由轉(zhuǎn)換到位置無序為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射。單位組的映射。 n一組位置一組位置P為為P1，P2，P3，P4，用圓圈代表位置。，用圓圈

12、代表位置。n一組轉(zhuǎn)換一組轉(zhuǎn)換T為為t1，t2，用短直線表示轉(zhuǎn)換。，用短直線表示轉(zhuǎn)換。n兩個用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭兩個用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭表示，它們是：表示，它們是：I(t1)=P2，P4，I(t2)=P2n兩個用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭兩個用于轉(zhuǎn)換的輸出函數(shù)，用由轉(zhuǎn)換指向位置的箭頭表示，它們是：表示，它們是：O(t1)=P1，O(t2)=P3，P3位置位置轉(zhuǎn)換轉(zhuǎn)換輸入輸入輸出輸出帶標記的帶標記的Petri網(wǎng)：網(wǎng)：通常，當每個通常，當每個輸入位置所擁有輸入位置所擁有的權(quán)標數(shù)大于等的權(quán)標數(shù)大于等于從該位置到轉(zhuǎn)于從該位置到轉(zhuǎn)換的線數(shù)時，就換的

13、線數(shù)時，就允許轉(zhuǎn)換。允許轉(zhuǎn)換。(1,2,0,1) (2,1,0,0) (2,0,2,0) 權(quán)標數(shù)權(quán)標數(shù)加入禁止線的加入禁止線的Petri網(wǎng)：網(wǎng)： 禁止線是用一個小圓圈而不是用箭頭標記禁止線是用一個小圓圈而不是用箭頭標記的輸入線。通常，當每個輸入線上至少有一個的輸入線。通常，當每個輸入線上至少有一個權(quán)標，而禁止線上沒有權(quán)標的時候，相應(yīng)的轉(zhuǎn)權(quán)標，而禁止線上沒有權(quán)標的時候，相應(yīng)的轉(zhuǎn)換才是允許的。換才是允許的。 禁止線禁止線輸入線輸入線4.4 Z語言語言4.4.1 簡介簡介 用用Z語言描述的、最簡單的形式化規(guī)格說語言描述的、最簡單的形式化規(guī)格說明含有下述明含有下述4個部分：個部分：n給定的集合、數(shù)據(jù)類

14、型及常數(shù)；給定的集合、數(shù)據(jù)類型及常數(shù)；n狀態(tài)定義；狀態(tài)定義；n初始狀態(tài)；初始狀態(tài)；n操作。操作。 1. 給定的集合給定的集合 一個一個Z規(guī)格說明從一系列給定的初始化集規(guī)格說明從一系列給定的初始化集合開始。所謂初始化集合就是不需要詳細定義合開始。所謂初始化集合就是不需要詳細定義的集合，這種集合用帶方括號的形式表示。對的集合，這種集合用帶方括號的形式表示。對于電梯問題，給定的初始化集合稱為于電梯問題，給定的初始化集合稱為Button，即所有按鈕的集合，因此，即所有按鈕的集合，因此，Z規(guī)格說明開始于：規(guī)格說明開始于：Button 2. 狀態(tài)定義狀態(tài)定義 一個一個Z規(guī)格說明由若干個規(guī)格說明由若干個“格

15、格(schema)”組成，每個格含有一組變量說明和一系列限定組成，每個格含有一組變量說明和一系列限定變量取值范圍的謂詞。變量取值范圍的謂詞。3. 初始狀態(tài)初始狀態(tài) 抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時的抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。對于電梯問題來說，抽象的初始狀態(tài)為：狀態(tài)。對于電梯問題來說，抽象的初始狀態(tài)為： Button_Init Button_Statepushed= 上式表示，當系統(tǒng)首次開啟時上式表示，當系統(tǒng)首次開啟時pushed集集為空，即所有按鈕都處于關(guān)閉狀態(tài)。為空，即所有按鈕都處于關(guān)閉狀態(tài)。4. 操作操作 如果一個原來處于關(guān)閉狀態(tài)的按鈕被按下，如果一個原來處于關(guān)閉狀態(tài)的按

16、鈕被按下，則該按鈕開啟，這個按鈕就被添加到則該按鈕開啟，這個按鈕就被添加到pushed集中。集中。4.4.2 評價評價(1) 可以比較容易地發(fā)現(xiàn)用可以比較容易地發(fā)現(xiàn)用Z寫的規(guī)格說明的錯誤。寫的規(guī)格說明的錯誤。(2) 用用Z寫規(guī)格說明時，要求作者十分精確地使用寫規(guī)格說明時，要求作者十分精確地使用Z說明說明符，減少了模糊性、不一致性和遺漏。符，減少了模糊性、不一致性和遺漏。(3) Z是一種形式化語言，在需要時開發(fā)者可以嚴格地驗是一種形式化語言，在需要時開發(fā)者可以嚴格地驗證規(guī)格說明的正確性。證規(guī)格說明的正確性。(4) 雖然完全學會雖然完全學會Z語言相當困難，但是，經(jīng)驗表明，只語言相當困難，但是，經(jīng)驗

17、表明，只學過中學數(shù)學的軟件開發(fā)人員仍然可以只用比較短的學過中學數(shù)學的軟件開發(fā)人員仍然可以只用比較短的時間就學會編寫時間就學會編寫Z規(guī)格說明。規(guī)格說明。(5) 使用使用Z語言可以降低軟件開發(fā)費用。語言可以降低軟件開發(fā)費用。 (6) 雖然用戶無法理解用雖然用戶無法理解用Z寫的規(guī)格說明，但是，可以依寫的規(guī)格說明，但是，可以依據(jù)據(jù)Z規(guī)格說明用自然語言重寫規(guī)格說明。規(guī)格說明用自然語言重寫規(guī)格說明。小結(jié)：小結(jié)：n基于數(shù)學的形式化規(guī)格說明技術(shù)，目前還沒有基于數(shù)學的形式化規(guī)格說明技術(shù)，目前還沒有在軟件產(chǎn)業(yè)界廣泛應(yīng)用，但它確實有實質(zhì)性的在軟件產(chǎn)業(yè)界廣泛應(yīng)用，但它確實有實質(zhì)性的優(yōu)點：形式化的規(guī)格說明可以用數(shù)學方法研究、優(yōu)點：形式化的規(guī)格說明可以用數(shù)學方法