軟件工程導(dǎo)論class5形式化說明技術(shù)

單擊此處編輯母版標(biāo)題樣式,,單擊此處編輯母版文本樣式,,第二級,,第三級,,第四級,,第五級,,,,*,,,單擊此處編輯母版標(biāo)題樣式,,單擊此處編輯母版文本樣式,,第二級,,第三級,,第四級,,第五級,,,,*,軟件工程導(dǎo)論第,5,課,第,4,章 形式化說明技術(shù),第,4,章 形式化說明技術(shù),軟件工程方法分類,,非形式化,,自然語言,,半形式化,,數(shù)據(jù)流圖,,實體,-,聯(lián)系圖建立模型,,形式化,,有窮狀態(tài)機,,,Petri,網(wǎng),,,Z,語言,,形式化方法,:,描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù),,4.1,概述,4.1.1,非形式化方法的缺點,,矛盾,：指一組相互沖突的陳述,,二義性,：讀者可以用不同方式理解的陳述,,含糊性,：系統(tǒng)規(guī)格說明書是很龐大的文檔,,,難以杜絕含糊性措辭,,不完整性,：對實體的描述不全面,,抽象層次混亂,：在非常抽象的陳述中混進了一些關(guān)于細節(jié)的低層次陳述,,,,4.1.2,形式化方法的優(yōu)點,理想的建模工具,,數(shù)學(xué)最有用的一個性質(zhì)是，它能夠簡潔準(zhǔn)確地描述物理現(xiàn)象、對象或動作的結(jié)果特別適于表示狀態(tài)在理想情況下，分析員可以寫出系統(tǒng)的數(shù)學(xué)規(guī)格說明， 它準(zhǔn)確到幾乎沒有二義性，而且可以用數(shù)學(xué)方法來驗 證，以發(fā)現(xiàn)存在的矛盾和不完整性，在這樣的規(guī)格說明 中完全沒有含糊性,4.1.2,形式化方法的優(yōu)點,可以在不同的軟件工程活動之間平滑地過渡,不僅功能規(guī)格說明，而且系統(tǒng)設(shè)計也可以用數(shù)學(xué)表達,,提供了高層確認(rèn)的手段,可以使用數(shù)學(xué)方法證明，設(shè)計符合規(guī)格說明，程序代碼 正確地實現(xiàn)了設(shè)計結(jié)果,,,,4.1.3,應(yīng)用形式化方法的準(zhǔn)則,形式化方法有爭議，要一分為二,,應(yīng)用形式化方法的準(zhǔn)則如下：,,(1),應(yīng)該選用適當(dāng)?shù)谋硎痉椒?。

一種規(guī)格說明技術(shù)只能用自然的方式說明某一類概念，適用于一定范圍,,(2),應(yīng)該形式化，但不要過分形式化,目前的形式化技術(shù)還不適于描述系統(tǒng)的每個方面主要,用形式化方法仔細說明系統(tǒng)中易出錯的或關(guān)鍵的部分,,,4.1.3,應(yīng)用形式化方法的準(zhǔn)則,(3),應(yīng)該估算成本,,為了使用形式化方法，通常需要事先進行大量的培訓(xùn),,(4),應(yīng)該有形式化方法顧問隨時提供咨詢,,絕大多數(shù)軟件工程師對形式化方法中使用的數(shù)學(xué)和邏輯 并不很熟悉，而且沒受過使用形式化方法的專業(yè)訓(xùn)練,,需要專家指導(dǎo)和培訓(xùn),,,4.1.3,應(yīng)用形式化方法的準(zhǔn)則,(5),不應(yīng)該放棄傳統(tǒng)的開發(fā)方法,,形式化方法和結(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋砜赡?取長補短,,(6),應(yīng)該建立詳盡的文檔,,使用自然語言注釋形式化的規(guī)格說明書，以幫助用戶和 維護人員理解系統(tǒng),,,4.1.3,應(yīng)用形式化方法的準(zhǔn)則,(7),不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn),,形式化方法僅僅有助于開發(fā)出高質(zhì)量軟件的一種手段,,,系統(tǒng)開發(fā)過程中仍然必須一如既往地實施其他質(zhì)量保證活動,,(8),不應(yīng)該盲目依賴形式化方法,,形式化方法并不能保證開發(fā)出的軟件絕對正確,,,，必須用其他方法,(,例如，評審、測試,),來驗證軟件正確性,,,4.1.3,應(yīng)用形式化方法的準(zhǔn)則,(9),應(yīng)該測試、測試再測試,,形式化方法不僅不能保證軟件系統(tǒng)絕對正確，也不能證明系統(tǒng)性能或其他質(zhì)量指標(biāo)符合需要，因此，軟件測試的重要性并沒有降低。

10),應(yīng)該重用,,軟件重用仍然是降低軟件成本和提高軟件質(zhì)量的惟一合理的方法形式化方法說明的軟件構(gòu)件具有清晰定義的功能和接 口，使得它們有更好的可重用性,,4.2,有窮狀態(tài)機,有窮狀態(tài)機可以準(zhǔn)確地描述一個系統(tǒng)，是表達規(guī)格說明的一種形式化方法,[,保險箱實例,],,一個保險箱上裝了一個復(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)盤的任何其他運動都將引起報警圖,4.1,描繪了保險箱的狀態(tài)轉(zhuǎn)換情況4.2.1,概念,,4.2.1,概念,,4.2.1,概念,有窮狀態(tài)機,5,部分,,狀態(tài)集,J,,輸入集,K,,轉(zhuǎn)換函數(shù),T:,由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個狀態(tài),(,次態(tài),),,初始態(tài),S,,終態(tài)集,F,,,?,,4.2.1,概念,有窮狀態(tài)機可以表示為一個,5,元組,(J,，,K,，,T,，,S,，,F),,J,是一個有窮的非空狀態(tài)集；,,K,是一個有窮的非空輸入集；,,T,是一個從,(J-F)×K,到,J,的轉(zhuǎn)換函數(shù)；,,S,∈,J,，是一個初始狀態(tài)；,,F,∈,J,，是終態(tài)集。

4.2.1,概念,[,保險箱實例,],,狀態(tài)集,J,：｛保險箱鎖定，,A,，,B,，保險箱解鎖，報警｝,,輸入集,K,：｛,1L,，,1R,，,2L,，,2R,，,3L,，,3R,｝,,轉(zhuǎn)換函數(shù),T,：如表,4.1,所示,,初始態(tài),S,：保險箱鎖定,,終態(tài)集,F,：｛保險箱解鎖，報警｝,,,,4.2.1,概念,有窮狀態(tài)機的應(yīng)用,,每個菜單驅(qū)動的用戶界面,:,一個菜單的顯示和一個狀態(tài)相對應(yīng)，鍵盤輸入或用鼠標(biāo)選擇一個圖標(biāo)是使系統(tǒng)進入其他狀態(tài) 的一個事件,,狀態(tài)的每個轉(zhuǎn)換都具有下面的形式：,,當(dāng)前狀態(tài),〔,菜單,〕,+,事件,〔,所選擇的項,〕 →,下個狀態(tài)當(dāng)前狀態(tài),〔,菜單,〕,+,事件,〔,所選擇的項,〕+,謂詞→ 下個狀態(tài),,增加一個謂詞集,P,，把有窮狀態(tài)機擴展為一個,6元組,,(J,，,K,，,T,，,S,，,F，P),,,,,,4.2.2,例子,用自然語言描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機描述的電梯系統(tǒng)需求,,,4.2.3,評價,有窮狀態(tài)機用簡單的格式來描述規(guī)格說明,,4.3 Petri,網(wǎng),Petri,網(wǎng),(Carl Adam Petri,發(fā)明,),用于確定系統(tǒng)中隱含的定時問題的一種有效技術(shù),,,用于解決如同步問題、競爭條件以及死鎖問題等問題,,應(yīng)用領(lǐng)域,,自動化,,性能評價,,操作系統(tǒng),,軟件工程 有效地描述,并發(fā)活動,,,,4.3.1,概念,Petri4,元素,,一組位置,P,,一組轉(zhuǎn)換,T,,輸入函數(shù),I,,輸出函數(shù),O,,P,為｛,P1,，,P2,，,P3,，,P4,｝，圓圈,,T,為｛,t1,，,t2,｝，短直線,,I(t1)=,｛,P2,，,P4,｝,I(t2)=,｛,P2,｝,,,位置指向轉(zhuǎn)換的箭頭,,O(t1)=,｛,P1,｝,O(t2)=,｛,P3,，,P3,｝,,,4.3.1,概念,形式化的,Petri,網(wǎng)結(jié)構(gòu)四元組,, 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)換到位置無序單位組的映射無序單位組或多重組是允許一個元素有多個實例的廣義集,,,4.3.1,概念,Petri,網(wǎng)的權(quán)標(biāo),·，,,見圖4.6,,P,1,中1個小黑點，P,2,中2個，P,4,中1 個,,可用向量表示,(1，2，0，1),,當(dāng)一個位置擁有的,權(quán)標(biāo)數(shù)大于等于,從它到轉(zhuǎn)換的,線數(shù),時，就允許轉(zhuǎn)換,,當(dāng),t,1,被激發(fā)，,P,2,和P,4,各有一個權(quán)標(biāo)被移走，P,1,增加一個權(quán)標(biāo),,4.3.1,概念,圖,4.7,上,P2有權(quán)標(biāo)，,,因此t2,也被激發(fā)，,,P2移走一個權(quán)標(biāo)，,,P3上新增加2個權(quán)標(biāo)，如圖4.8,所示,形式化說，,Petri,網(wǎng)是一組位置到一向量的映射,,M：P→{0,1，2，…},,帶有標(biāo)記的,Petri,網(wǎng)成為一個,5元組,,(P，T，I，O，M),4.3.1,概念,對,Petri,網(wǎng)的一個重要擴充是加入禁止線，禁止線用一個小圓圈標(biāo)記輸入線。

當(dāng)輸入線上至少有一個權(quán)標(biāo)，而禁止線上沒有權(quán)標(biāo)時，相應(yīng)的轉(zhuǎn)換才是允許的如圖,4.9,，,P,3,上有一個權(quán)標(biāo)而P,2,上沒有，,,因此轉(zhuǎn)換t,1,可以激發(fā)4.3.2,例子,F,f,表示樓層，電梯用權(quán)標(biāo)代表，在位置,F,f,有,權(quán)標(biāo),，表示在,樓層,f,上有電梯,電梯中樓層,f的按鈕，用位置EB,f,表示在,EB,f,,上有一個,權(quán)標(biāo),，表示,電梯內(nèi)樓層,f,的按鈕,被 按下了2,樓層按鈕,,4.4 Z,語言,在形式化的規(guī)格說明語言中，,Z語言贏得了廣泛的贊譽使用Z語言需要具備集合論、函數(shù)、數(shù)理邏輯等方面的知識Z語言是相當(dāng)難學(xué)的，因為它除了使用集合論,和數(shù)理邏輯符號外，還使用一些特殊符號4.4 .1,簡介,用Z語言描述的、最簡單的形式化規(guī)格說明含有下述4部分,,給定的集合、數(shù)據(jù)類型及常數(shù),,狀態(tài)定義,,初始狀態(tài),,操作,1,給定的集合,給定的初始化集合，就是不需要詳細定義的集合，用帶方括號的形式表示例如：電梯問題給定的初始化集合稱為,Button,,表示：,[Button],2,狀態(tài)定義,一個,Z規(guī)格說明由幾個格(schema),組成，每個格由一組變量說明和一系列限定變量取值范圍的謂詞，例如圖,4.12,,圖,4.13,是電梯例子的狀態(tài)定義,3,初始狀態(tài),第一次開啟時的狀態(tài),,電梯的初始狀態(tài),,,表示：當(dāng)系統(tǒng)首次開啟時,pushed,集為空，即所有的按鈕都處于關(guān)閉狀態(tài)。

4,操作,Z語言語法規(guī)定，當(dāng)一個格被,用在另一個格中時，要在它的前面加上一個三角形符號,,電梯的例子,,△,4,操作,電梯例子，到達樓層,,△,4.4.2,評價,Z語言成功的原因：,,(1)容易發(fā)現(xiàn)用Z寫的規(guī)格說明的錯誤,,(2)用Z寫規(guī)格說明時，要十分精確地使用Z說明符，減少了不一致性和遺漏3)可以嚴(yán)格地驗證說明的正確性4)學(xué)會編寫Z規(guī)格說明比較容易,,(5)減少開發(fā)總時間，減少費用,,(6)可以用自然語言重寫規(guī)格說明，說明更清楚，更正確。