軟件工程第4章

1、西安電子科技大學(xué)課程,第四章 形式化說明技術(shù)JSZX.XIDIAN.EDU.CN計算機信息應(yīng)用研究中心,第四章 形式化說明技術(shù),按照形式化的程度，可以把軟件工程使用的方法劃分成非形式化、半形式化和形式化3類。用自然語言描述需求規(guī)格說明，是典型的非形式化方法。用數(shù)據(jù)流圖或?qū)嶓w－聯(lián)系圖建立模型，是典型的半形式化方法。 所謂形式化方法，是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)，也就是說，如果一種方法有堅實的數(shù)學(xué)基礎(chǔ)，那么它就是

2、形式化的。4. 1 概述 4. 1. 1 非形式化方法的缺點 用自然語言書寫的系統(tǒng)規(guī)格說明書，可能存在矛盾、二義性、含糊性、不完整性及抽象層次混亂等問題。,第四章 形式化說明技術(shù),所謂矛盾是指一組相互沖突的陳述。 二義性是指讀者可以用不同方式理解的陳述。 不完整性可能是在系統(tǒng)規(guī)格說明中最常遇到的問題之一。 抽象層次混亂是指在非常抽象的陳述中混進了一些關(guān)于細(xì)節(jié)的低層次陳述。該規(guī)格說明書使

3、得讀者很難了解系統(tǒng)的整體功能結(jié)構(gòu)。4. 1. 2 形式化方法的優(yōu)點 人在理解用自然語言描述的規(guī)格說明時，容易產(chǎn)生二義性。為了克服非形式化方法的缺點，人們把數(shù)學(xué)引入軟件開發(fā)過程，創(chuàng)造了基于數(shù)學(xué)的形式化方法。在開發(fā)大型軟件系統(tǒng)的過程中應(yīng)用數(shù)學(xué)，能夠帶來下述的幾個優(yōu)點：,第四章 形式化說明技術(shù),數(shù)學(xué)最有用的一個性質(zhì)是，它能夠簡潔準(zhǔn)確地描述物理現(xiàn)象、對象或動作的結(jié)果，因此是理想的建模工具。數(shù)學(xué)特別適合于表示狀態(tài)，也就是表示“做什

4、么”。需求規(guī)格說明書主要描述應(yīng)用系統(tǒng)在運行前和運行后的狀態(tài)，因此，數(shù)學(xué)比自然語言更適合于描述詳細(xì)的需求。在理想的情況下，分析員可以寫出系統(tǒng)的數(shù)學(xué)規(guī)格說明書，它準(zhǔn)確到幾乎沒有二義性，而且可以用數(shù)學(xué)方法來驗證，以發(fā)現(xiàn)存在的矛盾和不完整性，在這樣的規(guī)格說明中完全沒有含糊性。 但是，實際情況并不這么簡單，希望用少數(shù)幾個數(shù)學(xué)公式來描述它，是根本不可能的。此外，即使應(yīng)用了形式化方法，完整性也是難于保證的：由于溝通不夠，可能遺漏了客戶的一些

5、需求；規(guī)格說明的撰寫者可能有意省略了系統(tǒng)的某些特征，以便設(shè)計者在選擇實現(xiàn)方法時有一定自由度；要設(shè)想出使用一個大型復(fù)雜系統(tǒng)的每一個可能的情景，通常是做不到的。,第四章 形式化說明技術(shù),在軟件開發(fā)過程中使用數(shù)學(xué)的另一個優(yōu)點是，可以在不同的軟件工程活動之間平滑地過渡。不僅功能規(guī)格說明，而且系統(tǒng)設(shè)計也可以用數(shù)學(xué)表達(dá)。 數(shù)學(xué)作為軟件開發(fā)工具的最后一個優(yōu)點是，它提供了高層確認(rèn)的手段?？梢允褂脭?shù)學(xué)方法證明，設(shè)計符合規(guī)格說明，程序代碼正確地

6、實現(xiàn)了設(shè)計結(jié)果。,第四章 形式化說明技術(shù),形式化規(guī)格說明語言構(gòu)成：1、語法：一般基于集合論、數(shù)理邏輯或代數(shù)學(xué)。 2、語義：是其所有語法符號的意義的數(shù)學(xué)描述。經(jīng)典的語義定義方法包括指稱語義、代數(shù)語義和操作語義方法。 3、推演規(guī)則：一般預(yù)期數(shù)學(xué)基礎(chǔ)和語義定義方法密切相關(guān)。規(guī)則必須在規(guī)格說明語言的語義系統(tǒng)中可證。因此，可以認(rèn)為規(guī)則是派生的語義定義，它們可以直接應(yīng)用于軟件規(guī)格說明的性質(zhì)證明并簡化推演過程。,第四章 形式化說明技術(shù),4

7、. 1. 3 應(yīng)用形式化方法的準(zhǔn)則 人們對形式化方法的看法并不一致。為了更好地發(fā)揮這種方法的長處，下面給出應(yīng)用形式化方法的幾條準(zhǔn)則，供讀者在實際工作中使用。 (1)應(yīng)該選用適當(dāng)?shù)谋硎痉椒?。通常，一種規(guī)格說明技術(shù)只能用自然的方式說明某一類概念，如果用這種技術(shù)描述其不適應(yīng)于描述的概念，則不僅工作量大而且描述方式也很復(fù)雜。例如，Z語言并不適于說明并發(fā)性。因此，應(yīng)該仔細(xì)選擇一種適用于當(dāng)前項目的形式化說明技術(shù)。 （2）

8、應(yīng)該形式化，但不要過分形式化。目前的形式化技術(shù)還不適于描述系統(tǒng)的每個方面。例如，示例屏幕和自然語言可能還是目前描述用戶界面的可視性的最佳方法。但是，也不能因此就認(rèn)為完全沒有必要采用形式化方法。形式化規(guī)格說明技術(shù)要求我們非常準(zhǔn)確地描述事物，因此有助于防止含糊和誤解。,第四章 形式化說明技術(shù),（3）應(yīng)該估算成本。為了使用形式化方法，通常需要事先進行大量的培訓(xùn)。最好預(yù)先估算所需的成本并編入預(yù)算。 （4）應(yīng)該有形式化方法顧問隨時提供咨

9、詢。絕大多數(shù)軟件工程師對形式化方法中使用數(shù)學(xué)和邏輯并不很熟悉，而且沒受過使用形式化方法的專業(yè)訓(xùn)練，因此，需要專家指導(dǎo)和培訓(xùn)。 （5）不應(yīng)該放棄傳統(tǒng)的開發(fā)方法。把形式化方法和結(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋硎强赡艿模矣捎谌￠L補短往往能獲得很好的效果。 （6）應(yīng)該建立詳盡的文檔。建議使用自然語言注釋形式化的規(guī)格說明書，以幫助用戶和維護人員理解系統(tǒng)。,第四章 形式化說明技術(shù),（7）不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)。形式化方法并不能保證

10、軟件的正確性，它們只不過是有助于開發(fā)出高質(zhì)量軟件的一種手段。除了使用形式化說明技術(shù)外，在系統(tǒng)開發(fā)過程中仍然必須一如既往地實施其他質(zhì)量保證活動。 （8）不應(yīng)該盲目依賴形式化方法。形式化方法并不能保證開發(fā)出的軟件絕對正確，例如，無法用形式化方法證明從非形式化需求到形式化規(guī)格說明的轉(zhuǎn)換是正確的，因此，必須用其他方法（例如，評審、測試）來驗證軟件正確性。 （9）應(yīng)該測試、測試再測試。形式化方法不僅不能保證軟件系統(tǒng)絕對正確，也不能

11、證明系統(tǒng)性能和其他質(zhì)量指標(biāo)符合要求，因此，軟件測試的重要性并沒有降低。 （10）應(yīng)該重用。即使采用了形式化方法，軟件重用仍然是降低軟件成本和提高軟件質(zhì)量的唯一合理的方法。而且用形式化方法說明的軟件構(gòu)件具有清晰定義的功能和接口，使得它們有更好的可重用性。,第四章 形式化說明技術(shù),4. 1. 4 形式化方法的分類 1、根據(jù)說明目標(biāo)軟件系統(tǒng)的方式，形式化方法可以分為兩類： 1）面向模型的形式化方法。面向模型的方法通過構(gòu)

12、造一個數(shù)學(xué)模型來說明系統(tǒng)的行為。 2）面向?qū)傩缘男问交椒?。面向?qū)傩缘姆椒ㄍㄟ^描述目標(biāo)軟件系統(tǒng)的各種屬性來間接定義系統(tǒng)行為。,第四章 形式化說明技術(shù),2、根據(jù)表達(dá)能力，形式化方法可以分為五類： 1）基于模型的方法：通過明確定義狀態(tài)和操作來建立一個系統(tǒng)模型（使系統(tǒng)從一個狀態(tài)轉(zhuǎn)換到另一個狀態(tài)）。用這種方法雖可以表示非功能性需求（諸如時間需求），但不能很好地表示并發(fā)性。如：Z語言，VDM，B方法等。 2）基

13、于邏輯的方法：用邏輯描述系統(tǒng)預(yù)期的性能，包括底層規(guī)約、時序和可能性行為。采用與所選邏輯相關(guān)的公理系統(tǒng)證明系統(tǒng)具有預(yù)期的性能。用具體的編程構(gòu)造擴充邏輯從而得到一種形式化方法，通過保持正確性的細(xì)化步驟集來開發(fā)系統(tǒng)。如：ITL（區(qū)間時序邏輯），區(qū)段演算（DC），模態(tài)邏輯，時序邏輯，TAM（時序代理模型），RTTL（實時時序邏輯）等。,第四章 形式化說明技術(shù),3）代數(shù)方法：通過將未定義狀態(tài)下不同的操作行為相聯(lián)系，給出操作的顯式定義。與基于模型

14、的方法相同的是，沒有給出并發(fā)的顯式表示。如：OBJ，Larch族代數(shù)規(guī)約語言等； 4）過程代數(shù)方法：通過限制所有容許的可觀察的過程間通信來表示系統(tǒng)行為。此類方法允許并發(fā)過程的顯式表示。如：通信順序過程（CSP），通信系統(tǒng)演算（CCS），通信過程代數(shù)（ACP），時序排序規(guī)約語言（LOTOS），計時CSP(TCSP），通信系統(tǒng)計時可能性演算（TPCCS）等。 5）基于網(wǎng)絡(luò)的方法：由于圖形化表示法易于理解，而且非專

15、業(yè)人員能夠使用，因此是一種通用的系統(tǒng)確定表示法。該方法采用具有形式語義的圖形語言，為系統(tǒng)開發(fā)和再工程帶來特殊的好處。如 Petri圖，計時Petri圖，狀態(tài)圖等。,第四章 形式化說明技術(shù),4. 1. 5 數(shù)學(xué)預(yù)備知識 1、集合和構(gòu)造規(guī)約 集合是對象或元素的聚集。集合論是形式化方法的基礎(chǔ)，集合中包含的元素是唯一的（即不允許重復(fù)）。具有少量的元素的集合用花括號（{，}）括起來，元素之間用逗號分開。例如：

16、 {7，14，3，12} ；包含4個自然數(shù)的集合 {7，14，7，3，12} ；該數(shù)的聚集不是集合，因為有7重復(fù)。 集合中的元素出現(xiàn)的順序是不重要的，集合中元素的數(shù)量稱為集合的基數(shù)，操作符#返回集合的基數(shù)，例如： #{7，14，3，12} = 4 ；其結(jié)果指出集合中項的數(shù)量。 有兩種定義集合的方式，一是通過枚舉出集合的元素來定義，二是創(chuàng)建一個構(gòu)造性集合規(guī)約，用布爾表

17、達(dá)式來刻劃集合成員的一般形式。因為集合規(guī)約可以為大集合提供簡潔的定義，比枚舉方式更受到青睞。,第四章 形式化說明技術(shù),例如，{n:N|n<3●n} 規(guī)約有三部分，基調(diào)n:N，一個謂詞n<3，以及一個項n。 基調(diào)刻劃在形成集合時考慮的值的范圍； 謂詞（布爾表達(dá)式）定義集合如何被構(gòu)造； 項則指出集合中項的一般形式。 N表示自然數(shù)，謂詞指出只有小于3的自然數(shù)被包含在集合

18、；項規(guī)定集合中每個元素的形式為n。 {0，1，2} ；集合形式是明顯的，則項可以省略。 上面的集合可表示為： {n:N|n<3},第四章 形式化說明技術(shù),集合元素可以是對，三元組，例如，集合定義為： { x , y:N| x +y = 10 *(x , y*2)}; 例如，第二個元素比第一個元素大3,并且第一個元素大于120，規(guī)約為：

19、 { n ：N| n > 120 *( n , n+3 )}; 當(dāng)然，表示某些計算機軟件成分所需的構(gòu)造性集合規(guī)約將比上面的例子復(fù)雜得多，然而，其基本形式和結(jié)構(gòu)是相同的。 2、集合的運算符 運算符∈用于表示集合中的成員關(guān)系。 例如，如果x是集合X中的成員，表達(dá)式x ∈ X 的值為真，否則其值為假。 謂詞：12 ∈{ 6，1，12，22 } 值為真，因為12 是集合中的成員。,第四

20、章 形式化說明技術(shù),運算符∈的反是運算符 如果x不是集合X的成員，表達(dá)式 x X的值為真，否則其值為假。 謂詞：13 ∈{ 6，1，13，122 } 值為假。 一個特殊的集合是空集φ，對應(yīng)普通數(shù)學(xué)中的0，空集具有它是所有集合的子集的性質(zhì)，兩個涉及空集的有用的等式是，對任何集合A： φ∪A=A和φ∩A=φ,,,第四章 形式化說明技術(shù),1．集合的交 由集合A和集合B的共同元

21、素組成的集合，叫做A與B的交集。寫作A∩B。 例如： （1）{3，6，9，12，15}∩{5，10，15，20，25}＝{15} （2）{二年級男生}∩{二年級三好學(xué)生}＝{二年級的男三好學(xué)生}用韋恩圖表示如下：（陰影部分表示交集） 如果集合A和集合B（都不是空集）沒有共同的元素。即A∩B＝ Ф ，我們就說A與B是不相交集。 例如：{1，3，5，7，9}∩{2，4，6，8，10}＝ Ф,第四

22、章 形式化說明技術(shù),2．集合的并 兩個集合A、B中的元素合在一起組成的新集合，叫做A與B的并集。寫作A∪B。 這里要注意，若A、B有共同的元素，只列舉一次。例如： A＝{數(shù)學(xué)小組同學(xué)}＝{李明，王平，張紅，宋軍} B＝{航模小組同學(xué)}＝{張紅，宋軍，何光，方強，劉華} A∪B＝{數(shù)學(xué)小組同學(xué)}∪{航模小組同學(xué)}　　 ＝{李明，王平，張紅，宋軍，何光，方強，劉華}用韋恩圖表示如下：（劃線部分

23、表示并集）,第四章 形式化說明技術(shù),若A、B是不相交的集，這兩個集合所有的元素合在一起就是它們的并集。 例如：{1，3，5，7}∪{2，4，6}＝{1，2，3，4，5，6，7} 從集合的觀點來看，加法運算就是求兩個不相交集的并集的基數(shù)。 例如，4＋3＝7。兩個不相交集的基數(shù)都叫做加數(shù)，加法的運算符號叫做加號。加得的結(jié)果，即兩個集的并集的基數(shù)，叫做和。,第四章 形式化說明技術(shù),序列是一種數(shù)學(xué)結(jié)構(gòu)

24、，對元素是有序的這一事實建模。 一個序列s是對的集合，它的元素從1到最高的數(shù)排序，例如：｛(1，Jones)，(2，Wilson)，(3，Shapiro)，(4，Estavez)｝ 形成對的第一個元素的項總稱為序列的定義域，第二個元素總稱為序列的值域。本書中序列用尖括號指明。例如，上面的序列寫作： ＜Jones，Wilson，Shapiro，Estavez＞ 和集合不同，序列中允許元素的重復(fù)，且序列的順序是重要

25、的。這樣有，〈Jones，Wilson，Shapiro〉≠〈Jones，Shapiro，Wilson〉和〈Jones， Wilson，Wilson〉≠〈Jones， Wilson〉 空序列表示為〈〉。 就集合而言還有集合的差，包含操作，子集等等；在形式化規(guī)約中同樣用到一組序列運算符。希望大家在實際工作之中用到時，能夠記得這些數(shù)學(xué)的基本概念和方法。,第四章 形式化說明技術(shù),4. 2 有窮狀態(tài)機

26、 4.2.1 概念 利用有窮狀態(tài)機可以準(zhǔn)確地描述一個系統(tǒng)，因此它是表達(dá)規(guī)格說明的一種形式化方法。 下面通過一個簡單的例子介紹有窮狀態(tài)機的基本概念。 一個保險箱上裝了一個復(fù)合鎖，鎖有三個位置，分別標(biāo)記為1、2、3，轉(zhuǎn)盤可向左（L）或向右（R）轉(zhuǎn)動。這樣，在任意時刻轉(zhuǎn)盤都有6種可能的運動，即1L、1R、2L、2R、3L和3R。保險箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤的任何其他運動都將引起報警

27、。,第四章 形式化說明技術(shù),教材P68頁圖4.1是一個有窮狀態(tài)機的狀態(tài)轉(zhuǎn)換圖。狀態(tài)轉(zhuǎn)換并不一定要用圖形方式描述，教材P68表4.1的表格形式也可以表達(dá)同樣的信息。除了兩個終態(tài)之外，保險箱的其他狀態(tài)將根據(jù)轉(zhuǎn)盤的轉(zhuǎn)動方式轉(zhuǎn)到下一個狀態(tài)。 從上面這個簡單例子可以看出，一個有窮狀態(tài)機包括下述5個部分：對于保險箱的例子，相應(yīng)的有窮狀態(tài)機的各部分如下。 狀態(tài)集J：{保險箱鎖定，A，B，保險箱解鎖，報警}。 輸入集K：

28、{1L,1R,2L,2R,3L,3R }。 轉(zhuǎn)換函數(shù)T：由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個狀態(tài)（次態(tài)），如表4.1所示。 初始態(tài)S：保險箱鎖定。 終態(tài)集F：{保險箱解鎖，報警}。,第四章 形式化說明技術(shù),一個有窮狀態(tài)機可以表示為一個5元組（J,K,T,S,T）, 其中： J 是一個有窮的非空狀態(tài)集； K 是一個有窮的非空輸入集； T 是一個從（J-F）*K到J的轉(zhuǎn)換函數(shù)；

29、 S ? J，是一個初始狀態(tài)； F J，是終態(tài)集。 有窮狀態(tài)機的概念在計算機系統(tǒng)中應(yīng)用得非常廣泛。例如，每個菜單驅(qū)動的用戶界面都是一個有窮狀態(tài)機的實現(xiàn)。一個菜單的顯示和一個狀態(tài)相對應(yīng)，鍵盤輸入或用鼠標(biāo)選擇一個圖標(biāo)是使系統(tǒng)進入其它狀態(tài)的一個事件。狀態(tài)的每個轉(zhuǎn)換都具有下面的形式： 當(dāng)前狀態(tài)［菜單］＋事件［所選擇的項］＝>下個狀態(tài)。 為了對一個系統(tǒng)進行規(guī)格說明,引入謂詞集P，從而把有窮狀態(tài)機擴展為一個6

30、元組，其中每個謂詞都是系統(tǒng)全局狀態(tài)Y的函數(shù)。轉(zhuǎn)換函數(shù)T現(xiàn)在是一個從（J-F）*K*P到J的函數(shù)?，F(xiàn)在的轉(zhuǎn)換規(guī)則形式如下： 當(dāng)前狀態(tài)［菜單］＋事件［所選擇的項］＋謂詞 = >下個狀態(tài),第四章 形式化說明技術(shù),4.2.2 例子 首先給出用自然語言描述的對電梯系統(tǒng)的需求： 在一幢m層的大廈中需要一套控制n部電梯的產(chǎn)品，要求這n部電梯按照約束條件C1，C2和C3在樓層間移動。 C1：每部電梯內(nèi)有m個按鈕，

31、每個按鈕代表一個樓層。當(dāng)按下一個按鈕時該按鈕指示燈亮，同時電梯駛向相應(yīng)的樓層，到達(dá)按鈕指定的樓層時指示燈熄滅。 C2：除了大廈的最低層和最高層之外，每層樓都有兩個按鈕分別請求電梯上行和下行。這兩個按鈕之一被按下時相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時燈熄滅，電梯向要求的方向移動。 C3：當(dāng)對電梯沒有請求時，它關(guān)門并停在當(dāng)前樓層。 現(xiàn)在使用一個擴展的有窮狀態(tài)機對本產(chǎn)品進行規(guī)格說明。這個問題中有兩個按鈕集:電梯按鈕

32、和樓層按鈕。,第四章 形式化說明技術(shù),電梯按鈕的狀態(tài)轉(zhuǎn)換圖如圖4.2所示。令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ā)光且電梯到達(dá)f層，該按鈕將熄滅。相反如果按鈕熄滅，則按下它時，按鈕將發(fā)光

33、。上述描述中包含了兩個事件，它們分別是： EBP(e,f)：電梯按鈕(e,f)被按下 EAF(e,f)：電梯e到達(dá)f層 為了定義與這些事件和狀態(tài)相聯(lián)系的狀態(tài)轉(zhuǎn)換規(guī)則，需要一個謂詞V(e,f)，它的含義如下： V(e,f)：電梯e停在f層 如果電梯按鈕(e,f)處于關(guān)閉狀態(tài)〔當(dāng)前狀態(tài)〕，而且電梯按鈕(e,f)被按下〔事件〕，而且電梯e不在f層〔謂詞〕，則該電梯按鈕打開發(fā)光〔下個狀態(tài)〕。

34、狀態(tài)轉(zhuǎn)換規(guī)則的形式化描述如下： EBOFF(e,f)+EBP(e,f)+not V(e,f) EBON(e,f) 反之，如果電梯到達(dá)f層，而且電梯按鈕是打開的，于是它就會熄滅。這條轉(zhuǎn)換規(guī)則可以形式化地表示為： EBON(e,f)+EAF(e,f)EBOFF(e,f),第四章 形式化說明技術(shù),圖4.2 電梯按鈕的狀態(tài)轉(zhuǎn)換圖圖4.3樓層按鈕的狀態(tài)轉(zhuǎn)換圖,第四章 形式化說明技術(shù),接下來考慮

35、樓層按鈕。令FB(d,f)表示f層請求電梯向d方向運動的按鈕，樓層按鈕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)閉的，被按下后該按鈕將打開。這段敘述中包含了以下兩個事件。 FBP(d,f)：樓層按鈕(d

36、,f)被按下 EAF(1…n,f)：電梯1或…或n到達(dá)f層 其中1…n表示或為1或為2…或為n。,第四章 形式化說明技術(shù),為了定義與這些事件和狀態(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)作為謂詞對待。使

37、用謂詞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層請求電梯向d方向運動的樓層按鈕處于關(guān)閉狀態(tài)，現(xiàn)在該按鈕被按下，并且當(dāng)時沒有正停在f層準(zhǔn)備向d方向移動的電梯，則該樓層按鈕打開。反之，如果樓

38、層按鈕已經(jīng)打開，且至少有一部電梯到達(dá)f層，該部電梯將朝d方向運動，則按鈕將關(guān)閉。 在討論電梯按鈕狀態(tài)轉(zhuǎn)換規(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),第四章 形式化說明技術(shù),定義電梯按鈕和樓層按鈕的狀態(tài)都是很簡單、直觀的事情?，F(xiàn)在轉(zhuǎn)向討論電梯的狀態(tài)及其轉(zhuǎn)換規(guī)則，就會出現(xiàn)一些復(fù)雜的情況。一個電梯狀態(tài)實質(zhì)上包含許多子狀

39、態(tài)。 下面定義電梯的3個狀態(tài)： M(d,e,f)：電梯e正沿d方向移動，即將到達(dá)的是第f層 S(d,e,f)：電梯e停在f層，將朝d方向移動(尚未關(guān)門) W(e,f)：電梯e在f層等待(已關(guān)門) 其中S(d,e,f)狀態(tài)已在討論樓層按鈕時定義過，但是，現(xiàn)在的定義更完備一些。 圖4.4是電梯的狀態(tài)轉(zhuǎn)換圖。3個電梯停止?fàn)顟B(tài)S(U,e,f)、S(N,e,f)和S(D,e,f

40、)已被組合成一個大的狀態(tài)，這樣做的目的是減少狀態(tài)總數(shù)以簡化流圖。 圖4.4中包含了下述3個可觸發(fā)狀態(tài)發(fā)生改變的事件。 DC(e,f)：電梯e在樓層f關(guān)上門 ST(e,f)：電梯e靠近f層時觸發(fā)傳感器，電梯控制器決定在當(dāng)前樓層電梯是否停下 RL：電梯按鈕或樓層按鈕被按下進入打開狀態(tài)，登錄需求,第四章 形式化說明技術(shù),圖4.4 電梯的狀態(tài)轉(zhuǎn)換圖,第四章 形式化說明技術(shù),最后，給出電梯的狀態(tài)轉(zhuǎn)換規(guī)則

41、。為簡單起見，這里給出的規(guī)則僅發(fā)生在關(guān)門之時。 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)備向上移動，且門已經(jīng)關(guān)閉，則電梯將向上一樓層移動。第二條和第三條規(guī)則，分別對應(yīng)于電梯即將下降或者沒有待處理的請求的情況。,第四章 形式化說明技術(shù),4. 2.3評

42、價 有窮狀態(tài)機方法采用了一種簡單的格式來描述規(guī)格說明： 當(dāng)前狀態(tài)+事件+謂詞下個狀態(tài) 這種形式的規(guī)格說明易于書寫、易于驗證，而且可以比較容易地把它轉(zhuǎn)變成設(shè)計或程序代碼。事實上，可以開發(fā)一個CASE工具把一個有窮狀態(tài)機規(guī)格說明直接轉(zhuǎn)變?yōu)樵创a。維護可以通過重新轉(zhuǎn)變來實現(xiàn)，也就是說，如果需要一個新的狀態(tài)或事件，首先修改規(guī)格說明，然后直接由新的規(guī)格說明生成新版本的產(chǎn)品。 有窮狀態(tài)機方法比數(shù)據(jù)流圖技術(shù)更

43、精確，而且和它一樣易于理解。不過，它也有缺點：在開發(fā)一個大系統(tǒng)時三元組(即狀態(tài)、事件、謂詞)的數(shù)量會迅速增長。此外，和數(shù)據(jù)流圖方法一樣，形式化的有窮狀態(tài)機方法也沒有處理定時需求。下節(jié)將介紹的Petri網(wǎng)技術(shù)，是一種可處理定時問題的形式化方法。,第四章 形式化說明技術(shù),4. 3　Petri網(wǎng) 4. 3. 1概念 并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題．這個問題可以表現(xiàn)為多種形式，如同步問題﹑競爭條件以及死鎖問題．定時問題通

44、常是由不好的設(shè)計或者有錯誤的實現(xiàn)引起的，而這些的設(shè)計和實現(xiàn)通常又是由不好的規(guī)格說明造成的．如果規(guī)格說明不當(dāng)，則有導(dǎo)致不完善的設(shè)計或?qū)崿F(xiàn)的危險．用于確定系統(tǒng)中隱含的定時問題的一種有效技術(shù)是Petri網(wǎng)，這種技術(shù)的一個很大的優(yōu)點是它也可以用于設(shè)計中． Petri網(wǎng)是由Carl　Adam　Petri發(fā)明的．最初只有自動化專家對Petri網(wǎng)感興趣，后來Petri網(wǎng)在計算機科學(xué)中也得到廣泛的應(yīng)用，例如，在性能評價﹑操作系統(tǒng)和軟件工程等領(lǐng)域

45、，Petri網(wǎng)應(yīng)用得都比較廣泛．特別是已經(jīng)證明，用Petri網(wǎng)可以有效地描述并發(fā)活動．,第四章 形式化說明技術(shù),Petri網(wǎng)包含４種元素：一組位置P﹑一組轉(zhuǎn)換T﹑輸入函數(shù)I和輸出函數(shù)O。教材P72圖４.５舉例說明了Petri網(wǎng)的組成．其中， 一組位置P，在圖中用圓圈代表位置． 一組轉(zhuǎn)換T，在圖中用短直線表示轉(zhuǎn)換． 兩個用于轉(zhuǎn)換的輸入函數(shù)，用由位置指向轉(zhuǎn)換的箭頭表示，它們是： I(t1)= {P2，P4}

46、 I(t2)= {P2} 兩個用于轉(zhuǎn)換的輸出函數(shù)，用有轉(zhuǎn)換指向位置的箭頭表示，它們是： O（t1）={P1} O（t2）={P3，P3} 注意輸出函數(shù)O(t2)中有兩個 P3，是因為有兩個箭頭有t2指向P3。,第四章 形式化說明技術(shù),更形式化的Petri網(wǎng)結(jié)構(gòu)，是一個四元組C=(P,T,I,O)。其中， P={P1，...，Pn}是一個有窮位置集，n>=0。

47、 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)的標(biāo)記是在Petri網(wǎng)中權(quán)標(biāo)（token）的分配。例如，在教材P73圖4.6中有4個權(quán)標(biāo)，其中一個在P1

48、中，兩個在P2中，P3中沒有，還有一個在P4中。上述標(biāo)記可以用向量（1，2，0，1）表示。由于P2和P4中有權(quán)標(biāo)，因此t1啟動（即被激發(fā)）。通常，當(dāng)每個輸入位置所擁有的權(quán)標(biāo)數(shù)大于等于從該位置到轉(zhuǎn)換的線數(shù)時，就允許轉(zhuǎn)換。當(dāng)t1被激發(fā)時，P2和P4上各有一個權(quán)標(biāo)被移出，P1上增加一個權(quán)標(biāo)。Petri網(wǎng)中權(quán)標(biāo)總數(shù)不是固定的，在這個例子中兩個權(quán)標(biāo)被移出，而P1上只能增加一個權(quán)標(biāo)。,第四章 形式化說明技術(shù),圖4.6 帶標(biāo)記的Petri網(wǎng)

49、 圖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),第四章 形式化說明技術(shù),教材P73頁圖4.6中P2上有權(quán)標(biāo)，因此t2也可以被激發(fā)。當(dāng)t2被激發(fā)時，P2上將移走一個權(quán)標(biāo)，而P3上新增加兩

50、個權(quán)標(biāo)。Petri網(wǎng)具有非確定性，也就是說，如果數(shù)個轉(zhuǎn)換都達(dá)到了激發(fā)條件，則其中任意一個都可以被激發(fā)。 教材P73頁圖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）。此時，只有t2可以被激發(fā)。如果t2也被激發(fā)了，則權(quán)標(biāo)從P2中移出，兩個新權(quán)標(biāo)被放在P3上，結(jié)果如圖4.8所示，標(biāo)記為（2，0，2，0）。,第四章 形式化說明技術(shù),

51、更形式化的說，Petri網(wǎng)C=(P，T，I，O)中的標(biāo)記M，是有一組位置P到一組非負(fù)數(shù)的映射： M：→ P{0，1，2，...} 這樣，帶有標(biāo)記的Petri網(wǎng)成為一個五元組（P，T，I，O，M）。 對Petri網(wǎng)的一個重要擴充是加入禁止線。如圖4.9所示，禁止線是用一個小圓圈而不是用箭頭標(biāo)記的輸入線。通常，當(dāng)每個輸入線上至少有一個標(biāo)權(quán)，而禁止線上沒有標(biāo)權(quán)，因此轉(zhuǎn)換t1可以被激發(fā)。,第四章 形式化說明技術(shù),

52、動態(tài)轉(zhuǎn)移特征,網(wǎng)論的觀點認(rèn)為，解決沖突的辦法可以是，通過環(huán)境對系統(tǒng)進行控制。這里有兩種可能：若t1發(fā)生，p1失去標(biāo)記，p2獲得標(biāo)記，這時只有t2可以發(fā)生，之后標(biāo)記回到p1。這時若再讓t1發(fā)生，則會重復(fù)上述過程。若讓t3發(fā)生，p1失去標(biāo)記，p3和p4同時各得一個標(biāo)記。這時t4和t5都可以發(fā)生，且互不影響，網(wǎng)論中稱這種現(xiàn)象為“并發(fā)”(concurrent)，t4和t5發(fā)生以后，t6可以發(fā)生，使標(biāo)記又回到p1，p6起著使t4和t5兩個異步活動

53、同步的作用。,圖中的Petri網(wǎng)，只有p1中有一個標(biāo)記，從這個給定的初始標(biāo)識看，t1和t3都能發(fā)生，但不能同時發(fā)生，因為它們共享p1中的一個資源，這種現(xiàn)象叫做“沖突”（conflict）。,第四章 形式化說明技術(shù),如果讓p1和p3各有一個標(biāo)記，并規(guī)定位置容量均不能超過1，這時t3不能發(fā)生，因為t3的發(fā)生會使p3的容量超過1，稱這種現(xiàn)象為“碰撞”（contact）。 有時，一個Petri網(wǎng)中同時存在著并發(fā)和沖突，而且并發(fā)的實施

54、會引起沖突的消失（減少）或出現(xiàn)（增加），我們稱這種情況為“混惑”（confusion）。,在圖示Petri網(wǎng)中，t1和t3是兩個并發(fā)事件，如果t1實際上在t3之前發(fā)生，則t2不會發(fā)生沖突；反之，則發(fā)生沖突。所以存在著“混惑”的系統(tǒng)是不好的系統(tǒng)，因為在這種系統(tǒng)中，沖突忽隱忽現(xiàn)，使得外部環(huán)境對系統(tǒng)難以控制。,第四章 形式化說明技術(shù),4.3.2 例子 現(xiàn)在把Petri網(wǎng)應(yīng)用于上一節(jié)討論過的電梯問題。當(dāng)用Petri網(wǎng)表示電梯系

55、統(tǒng)的規(guī)格說明時，每個樓層用一個位置Ff代表(1≤f≤m)，在Petri網(wǎng)中電梯是用一個權(quán)標(biāo)代表的。在位置Ff上有權(quán)標(biāo)，表示在樓層f上有電梯。 1. 電梯按鈕 電梯問題的第一個約束條件描述了電梯按鈕的行為，現(xiàn)在復(fù)述一下這個約束條件。 第一條約束C1：每部電梯有m個按鈕，每層對應(yīng)一個按鈕。當(dāng)按下一個按鈕時該按鈕指示燈亮，指示電梯移往相應(yīng)的樓層。當(dāng)電梯到達(dá)指定的樓層時，按鈕將熄滅。,第四章 形式化說明技術(shù),為了用Pet

56、ri網(wǎng)表達(dá)電梯按鈕的規(guī)格說明，在Petri網(wǎng)中還必須設(shè)置其他的位置。電梯中樓層f的按鈕，在Petri網(wǎng)中用位置EBf表示(1≤f≤m)。在EBf上有一個權(quán)標(biāo)，就表示電梯內(nèi)樓層f的按鈕被按下了。 電梯按鈕只有在第一次被按下時才會由暗變亮，以后再按它則只會被忽略。圖4.10所示的Petri網(wǎng)準(zhǔn)確地描述了電梯按鈕的行為規(guī)律。首先，假設(shè)按鈕沒有發(fā)亮，顯然在位置EBf上沒有權(quán)標(biāo)，從而在存在禁止線的情況下，轉(zhuǎn)換“EBf被按下”是允許發(fā)生的

57、。假設(shè)現(xiàn)在按下按鈕，則轉(zhuǎn)換被激發(fā)并在EBf上放置了一個權(quán)標(biāo)，如圖4.10所示。以后不論再按下多少次按鈕，禁止線與現(xiàn)有權(quán)標(biāo)的組合都決定了轉(zhuǎn)換“EBf被按下”不能再被激發(fā)了，因此，位置EBf上的權(quán)標(biāo)數(shù)不會多于1。,第四章 形式化說明技術(shù),圖4.10 Petri網(wǎng)表示的電梯按鈕,第四章 形式化說明技術(shù),假設(shè)電梯由g層駛向f層，因為電梯在g層，如圖4.10所示，位置Fg上有一個權(quán)標(biāo)。由于每條輸入線上各有一個權(quán)標(biāo)，轉(zhuǎn)換“電梯在運行”被激發(fā)，從

58、而EBf和Fg上的權(quán)標(biāo)被移走，按鈕EBf被關(guān)閉，在位置Ff上出現(xiàn)一個新權(quán)標(biāo)，即轉(zhuǎn)換的激發(fā)使電梯由g層駛到f層。 事實上，電梯由g層移到f層是需要時間的，為處理這個情況及其他類似的問題(例如，由于物理上的原因按鈕被按下后不能馬上發(fā)亮)，Petri網(wǎng)模型中必須加入時限。也就是說，在標(biāo)準(zhǔn)Petri網(wǎng)中轉(zhuǎn)換是瞬時完成的，而在現(xiàn)實情況下就需要時間控制Petri網(wǎng)，以使轉(zhuǎn)換與非零時間相聯(lián)系。,第四章 形式化說明技術(shù),2. 樓層按鈕

59、 在第二個約束條件中描述了樓層按鈕的行為。 第二條約束C2：除了第一層與頂層之外，每個樓層都有兩個按鈕，一個要求電梯上行，另一個要求電梯下行。這些按鈕在按下時發(fā)亮，當(dāng)電梯到達(dá)該層并將向指定方向移動時，相應(yīng)的按鈕才會熄滅。 在Petri網(wǎng)中樓層按鈕用位置FBfu和FBfd表示，分別代表f樓層請求電梯上行和下行的按鈕。底層的按鈕為FB1u，最高層的按鈕為FBmd，中間每一層有兩個按鈕FBfu和FBfd(1＜f＜m)。,第四

60、章 形式化說明技術(shù),圖4.11 Petri網(wǎng)表示樓層按鈕,第四章 形式化說明技術(shù),圖4.11所示的情況為電梯由g層駛向f層。根據(jù)電梯乘客的要求，某一個樓層按鈕亮或兩個樓層按鈕都亮。如果兩個按鈕都亮了，則只有一個按鈕熄滅。圖4.11所示的Petri網(wǎng)可以保證，當(dāng)兩個按鈕都亮了的時候，只有一個按鈕熄滅。但是要保證按鈕熄滅正確，則需要更復(fù)雜的Petri網(wǎng)模型。 最后，考慮第三條約束。 第三條約束C3：當(dāng)電梯沒有收到請求時，

61、它將停留在當(dāng)前樓層并關(guān)門。 這條約束很容易實現(xiàn)，如圖4.11所示，當(dāng)沒有請求(FBfu和FBfd上無權(quán)標(biāo)）時，任何一個轉(zhuǎn)換“電梯在運行”都不能被激發(fā)。,第四章 形式化說明技術(shù),4.4  Z 語言  在形式化的規(guī)格說明語言中，Z語言贏的了廣泛的贊譽。使用Z語言需要具備集合論、函數(shù)、數(shù)理邏輯等方面的知識。即使用戶已經(jīng)掌握了所需要的背景知識，Z語言也是相當(dāng)難學(xué)的，因為它除了使用常用的集合論和數(shù)理邏

62、輯符號之外，還使用了一些特殊符號。4.4.1 簡介 本節(jié)結(jié)合電梯問題的例子，簡要的介紹Z語言。 用Z語言描述的、最簡單的形式化規(guī)格說明含有下述4個部分： 1.給定的集合、數(shù)據(jù)類型及常數(shù)。 2.狀態(tài)定義。 3.初始狀態(tài)。 4.操作。,第四章 形式化說明技術(shù),1．給定的集合 一個Z規(guī)則說明從一系列給定的初始化集合開始。所謂初始化集合就是不需要詳細(xì)定義的集合，這種集

63、合用帶方括號的形式標(biāo)識。對于電梯問題，給定的初始化集合稱為Button，即所有按鈕的集合，因此，Z規(guī)則說明開始于：[Button] 2．狀態(tài)定義 一個Z規(guī)則說明有若干個“格”組成，每個格含有一組變量說明和一系列限定變量取值范圍的謂詞。例如，格S的格式圖教材P76頁圖4.12所示。,第四章 形式化說明技術(shù),Z格S的格式,在電梯問題中，Button有4個子集，即floor_buttons（樓層按鈕的集合）、elev

64、ator_buttons（電梯按鈕的集合）、buttons（電梯問題中所有按鈕的集合）以及pushed（所有被按的按鈕的的集合，即所有處于打開狀態(tài)的按鈕的集合）。 教材P76頁圖4.13描述了格Button_State,其中，符號P表示冪集（即給定集的所有子集），約束條件聲明，floor_buttons集與elebator_buttons集不相交，共同組成buttons集（把它們放于教材P76頁圖4.13中只是用來說明Z格包含

65、的內(nèi)容）。,第四章 形式化說明技術(shù),3．初始狀態(tài) 抽象的初始狀態(tài)是指系統(tǒng)第一次開啟時的狀態(tài)。對于電梯問題來說，抽象的初始狀態(tài)為： Button_Init＝［Button_State｜pushed= Ф ］ 上式表示，當(dāng)系統(tǒng)首次開啟時pushed集為空，即所有按鈕都處于關(guān)閉狀態(tài)。 4．操作 如果一個原來處與關(guān)閉狀態(tài)的按鈕被按下，則該按鈕開啟，這個按鈕就被添加到pushed集中。教材P77

66、頁圖4.14定義了操作Push_Button（按按鈕）。Z語言的語法規(guī)定，當(dāng)一個格被用在另一個格中時，要在它前面加上三角形符號Δ作為前綴，因此，格Push_Button的第一行最前面有一個三角形符號作為格Button_State的前綴。操作Push_Button有一個輸入變量“button?”。問號“？”表示輸入變量，而感嘆號“！”代表輸出變量。,第四章 形式化說明技術(shù),操作的謂詞部分，包含了一組調(diào)用操作的前置條件，以及操作完全結(jié)束后

67、的后置條件。如果前置條件成立，則操作執(zhí)行完成后可得到后置條件。但是，如果在前置條件不成立的條件下調(diào)用該操作，則不能得到指定的結(jié)果。（因此結(jié)果無法預(yù)測） 教材P77頁圖4.14中的第一個前置條件規(guī)定，“button?”必須是buttons的一個元素，而buttons是電梯系統(tǒng)中所有按鈕的集合。如果第二個前置條件button? Pushed得到滿足（即按鈕沒有開啟），則更新pushed按鈕集，使之包含剛開啟的按鈕“but

68、ton?”。在Z語言中，當(dāng)一個變量的值發(fā)生改變時，就用符號“′”表示。也就是說，后置條件是當(dāng)執(zhí)行完操作Push_Button之后，“button?”將被加入到pushed集中。無需直接打開按鈕，只要使“button?”變成pushed中的一個元素即可。,第四章 形式化說明技術(shù),還有一種可能性是，被按的按鈕原先已經(jīng)被打開。由于button? ∈pushed，根據(jù)第三個前置條件，將沒有任何事情發(fā)生，這可以用pushed′=pushed來表

69、示，即pushed的新狀態(tài)和舊狀態(tài)一樣。注意。如果沒有第三個前置條件，規(guī)格說明將不能說明在一個按鈕已被按過之后又被按了一次的情況下將發(fā)生什么事，因此，結(jié)果將是不可預(yù)測的。 假設(shè)電梯達(dá)到了某樓層，如果相應(yīng)的樓層按鈕已經(jīng)打開，則此時它會關(guān)閉；同樣，如果相應(yīng)的電梯按鈕已經(jīng)打開，則此時它會關(guān)閉。也就是說，如果“button?”屬于pushed集，則將它移出該集合，如教材P77頁圖4.15所示（符號“\”表示集合差運算）。但是，如果按鈕