《軟件工程導(dǎo)論class5形式化說(shuō)明技術(shù)》由會(huì)員分享，可在線閱讀，更多相關(guān)《軟件工程導(dǎo)論class5形式化說(shuō)明技術(shù)（43頁(yè)珍藏版）》請(qǐng)?jiān)谘b配圖網(wǎng)上搜索。

1、,,單擊此處編輯母版標(biāo)題樣式,,單擊此處編輯母版文本樣式,,第二級(jí),,第三級(jí),,第四級(jí),,第五級(jí),,,,*,,,單擊此處編輯母版標(biāo)題樣式,,單擊此處編輯母版文本樣式,,第二級(jí),,第三級(jí),,第四級(jí),,第五級(jí),,,,*,軟件工程導(dǎo)論第,5,課,第,4,章 形式化說(shuō)明技術(shù),第,4,章 形式化說(shuō)明技術(shù),軟件工程方法分類,,非形式化,,自然語(yǔ)言,,半形式化,,數(shù)據(jù)流圖,,實(shí)體,-,聯(lián)系圖建立模型,,形式化,,有窮狀態(tài)機(jī),,,Petri,網(wǎng),,,Z,語(yǔ)言,,形式化方法,:,描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù),,4.1,概述,4.1.1,非形式化方法的缺點(diǎn),,矛盾,：指一組相互沖突的陳述,,二義性,：讀者可

2、以用不同方式理解的陳述,,含糊性,：系統(tǒng)規(guī)格說(shuō)明書是很龐大的文檔,,,難以杜絕含糊性措辭,,不完整性,：對(duì)實(shí)體的描述不全面,,抽象層次混亂,：在非常抽象的陳述中混進(jìn)了一些關(guān)于細(xì)節(jié)的低層次陳述,,,,4.1.2,形式化方法的優(yōu)點(diǎn),理想的建模工具,,數(shù)學(xué)最有用的一個(gè)性質(zhì)是，它能夠簡(jiǎn)潔準(zhǔn)確地描述物理現(xiàn)象、對(duì)象或動(dòng)作的結(jié)果。特別適于表示狀態(tài)。,,在理想情況下，分析員可以寫出系統(tǒng)的數(shù)學(xué)規(guī)格說(shuō)明， 它準(zhǔn)確到幾乎沒有二義性，而且可以用數(shù)學(xué)方法來(lái)驗(yàn) 證，以發(fā)現(xiàn)存在的矛盾和不完整性，在這樣的規(guī)格說(shuō)明 中完全沒有含糊性,4.1.2,形式化方法的優(yōu)點(diǎn),可以在不同的軟件工程活動(dòng)之間平滑地過渡,不僅功能規(guī)格說(shuō)明，而且系

3、統(tǒng)設(shè)計(jì)也可以用數(shù)學(xué)表達(dá),,提供了高層確認(rèn)的手段,可以使用數(shù)學(xué)方法證明，設(shè)計(jì)符合規(guī)格說(shuō)明，程序代碼 正確地實(shí)現(xiàn)了設(shè)計(jì)結(jié)果,,,,4.1.3,應(yīng)用形式化方法的準(zhǔn)則,形式化方法有爭(zhēng)議，要一分為二,,應(yīng)用形式化方法的準(zhǔn)則如下：,,(1),應(yīng)該選用適當(dāng)?shù)谋硎痉椒?。一種規(guī)格說(shuō)明技術(shù)只能用自然的方式說(shuō)明某一類概念，適用于一定范圍,,(2),應(yīng)該形式化，但不要過分形式化,。目前的形式化技術(shù)還不適于描述系統(tǒng)的每個(gè)方面。,,,主要,用形式化方法仔細(xì)說(shuō)明系統(tǒng)中易出錯(cuò)的或關(guān)鍵的部分,,,4.1.3,應(yīng)用形式化方法的準(zhǔn)則,(3),應(yīng)該估算成本,,為了使用形式化方法，通常需要事先進(jìn)行大量的培訓(xùn),,(4),應(yīng)該有形式化方

4、法顧問隨時(shí)提供咨詢,,絕大多數(shù)軟件工程師對(duì)形式化方法中使用的數(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ū)ο蠓椒善饋?lái)可能 取長(zhǎng)補(bǔ)短,,(6),應(yīng)該建立詳盡的文檔,,使用自然語(yǔ)言注釋形式化的規(guī)格說(shuō)明書，以幫助用戶和 維護(hù)人員理解系統(tǒng),,,4.1.3,應(yīng)用形式化方法的準(zhǔn)則,(7),不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn),,形式化方法僅僅有助于開發(fā)出高質(zhì)量軟件的一種手段,,,系統(tǒng)開發(fā)過程中仍然必須一如既往地實(shí)施其他質(zhì)量保證活動(dòng),,(8),不應(yīng)該盲目依賴形式化方法,,形式化方法并

5、不能保證開發(fā)出的軟件絕對(duì)正確,,,，必須用其他方法,(,例如，評(píng)審、測(cè)試,),來(lái)驗(yàn)證軟件正確性,,,4.1.3,應(yīng)用形式化方法的準(zhǔn)則,(9),應(yīng)該測(cè)試、測(cè)試再測(cè)試,,形式化方法不僅不能保證軟件系統(tǒng)絕對(duì)正確，也不能證明系統(tǒng)性能或其他質(zhì)量指標(biāo)符合需要，因此，軟件測(cè)試的重要性并沒有降低。,,(10),應(yīng)該重用,,軟件重用仍然是降低軟件成本和提高軟件質(zhì)量的惟一合理的方法。形式化方法說(shuō)明的軟件構(gòu)件具有清晰定義的功能和接 口，使得它們有更好的可重用性,,4.2,有窮狀態(tài)機(jī),有窮狀態(tài)機(jī)可以準(zhǔn)確地描述一個(gè)系統(tǒng)，是表達(dá)規(guī)格說(shuō)明的一種形式化方法,。,,[,保險(xiǎn)箱實(shí)例,],,一個(gè)保險(xiǎn)箱上裝了一個(gè)復(fù)合鎖，鎖有三個(gè)位置

6、，分別標(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.2.1,概念,,4.2.1,概念,,4.2.1,概念,有窮狀態(tài)機(jī),5,部分,,狀態(tài)集,J,,輸入集,K,,轉(zhuǎn)換函數(shù),T:,由當(dāng)前狀態(tài)和當(dāng)前輸入確定下一個(gè)狀態(tài),(,次態(tài),),,初始態(tài),S,,終態(tài)集,F,,,?,,4.2.1,概念,有窮狀態(tài)機(jī)可以表示為一個(gè),5,元組,(J,，,K,，,T,，,

7、S,，,F),,J,是一個(gè)有窮的非空狀態(tài)集；,,K,是一個(gè)有窮的非空輸入集；,,T,是一個(gè)從,(J-F)×K,到,J,的轉(zhuǎn)換函數(shù)；,,S,∈,J,，是一個(gè)初始狀態(tài)；,,F,∈,J,，是終態(tài)集。,,,4.2.1,概念,[,保險(xiǎn)箱實(shí)例,],,狀態(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)警｝,,,,4.2.1,概念,有窮狀態(tài)機(jī)的應(yīng)用,,每個(gè)菜單驅(qū)動(dòng)的用戶界面,:,一個(gè)菜單的顯示和一個(gè)狀態(tài)相對(duì)應(yīng)，鍵盤輸入或

8、用鼠標(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)。,,當(dāng)前狀態(tài),〔,菜單,〕,+,事件,〔,所選擇的項(xiàng),〕+,謂詞→ 下個(gè)狀態(tài),,增加一個(gè)謂詞集,P,，把有窮狀態(tài)機(jī)擴(kuò)展為一個(gè),6元組,,(J,，,K,，,T,，,S,，,F，P),,,,,,4.2.2,例子,用自然語(yǔ)言描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機(jī)描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機(jī)描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機(jī)描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機(jī)描述的電梯系統(tǒng)需

9、求,,4.2.2,例子,用有窮狀態(tài)機(jī)描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機(jī)描述的電梯系統(tǒng)需求,,4.2.2,例子,用有窮狀態(tài)機(jī)描述的電梯系統(tǒng)需求,,,4.2.3,評(píng)價(jià),有窮狀態(tài)機(jī)用簡(jiǎn)單的格式來(lái)描述規(guī)格說(shuō)明,,4.3 Petri,網(wǎng),Petri,網(wǎng),(Carl Adam Petri,發(fā)明,),用于確定系統(tǒng)中隱含的定時(shí)問題的一種有效技術(shù),,,用于解決如同步問題、競(jìng)爭(zhēng)條件以及死鎖問題等問題,,應(yīng)用領(lǐng)域,,自動(dòng)化,,性能評(píng)價(jià),,操作系統(tǒng),,軟件工程 有效地描述,并發(fā)活動(dòng),,,,4.3.1,概念,Petri4,元素,,一組位置,P,,一組轉(zhuǎn)換,T,,輸入函數(shù),I,,輸出函數(shù),O,,P

10、,為｛,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,｝是一個(gè)有窮位置集，,n,≥,0,。,,T=,｛,t1,，,…,，,tm,｝是一個(gè)有窮轉(zhuǎn)換集，,m,≥,0,，且,T,和,P,不相交。,,I,：,T,→,P,∞為輸入函數(shù)，是由轉(zhuǎn)換到位置無(wú)序單位組,(bags),的映射。

11、,,O,：,T,→,P,∞為輸出函數(shù)，是由轉(zhuǎn)換到位置無(wú)序單位組的映射。,,無(wú)序單位組或多重組是允許一個(gè)元素有多個(gè)實(shí)例的廣義集,,,4.3.1,概念,Petri,網(wǎng)的權(quán)標(biāo),·，,,見圖4.6,,P,1,中1個(gè)小黑點(diǎn)，P,2,中2個(gè)，P,4,中1 個(gè),,可用向量表示,(1，2，0，1),,當(dāng)一個(gè)位置擁有的,權(quán)標(biāo)數(shù)大于等于,從它到轉(zhuǎn)換的,線數(shù),時(shí)，就允許轉(zhuǎn)換,,當(dāng),t,1,被激發(fā)，,P,2,和P,4,各有一個(gè)權(quán)標(biāo)被移走，P,1,增加一個(gè)權(quán)標(biāo),,4.3.1,概念,圖,4.7,上,P2有權(quán)標(biāo)，,,因此t2,也被激發(fā)，,,P2移走一個(gè)權(quán)標(biāo)，,,P3上新增加2個(gè)權(quán)標(biāo)，如圖4.8,所示,。,,形式化說(shuō)，,Pe

12、tri,網(wǎng)是一組位置到一向量的映射,,M：P→{0,1，2，…},,帶有標(biāo)記的,Petri,網(wǎng)成為一個(gè),5元組,,(P，T，I，O，M),4.3.1,概念,對(duì),Petri,網(wǎng)的一個(gè)重要擴(kuò)充是加入禁止線，禁止線用一個(gè)小圓圈標(biāo)記輸入線。當(dāng)輸入線上至少有一個(gè)權(quán)標(biāo)，而禁止線上沒有權(quán)標(biāo)時(shí)，相應(yīng)的轉(zhuǎn)換才是允許的。如圖,4.9,，,P,3,上有一個(gè)權(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,,上有一個(gè),權(quán)標(biāo),，表示,電梯內(nèi)樓層,

13、f,的按鈕,被 按下了。,,,2,樓層按鈕,,4.4 Z,語(yǔ)言,在形式化的規(guī)格說(shuō)明語(yǔ)言中，,Z語(yǔ)言贏得了廣泛的贊譽(yù)。使用Z語(yǔ)言需要具備集合論、函數(shù)、數(shù)理邏輯等方面的知識(shí)。,,Z語(yǔ)言是相當(dāng)難學(xué)的，因?yàn)樗耸褂眉险?和數(shù)理邏輯符號(hào)外，還使用一些特殊符號(hào)。,4.4 .1,簡(jiǎn)介,用Z語(yǔ)言描述的、最簡(jiǎn)單的形式化規(guī)格說(shuō)明含有下述4部分,,給定的集合、數(shù)據(jù)類型及常數(shù),,狀態(tài)定義,,初始狀態(tài),,操作,1,給定的集合,給定的初始化集合，就是不需要詳細(xì)定義的集合，用帶方括號(hào)的形式表示。,,例如：電梯問題給定的初始化集合稱為,Button,,表示：,[Button],2,狀態(tài)定義,一個(gè),Z規(guī)格說(shuō)明由幾個(gè)格(sc

14、hema),組成，每個(gè)格由一組變量說(shuō)明和一系列限定變量取值范圍的謂詞，例如圖,4.12,,圖,4.13,是電梯例子的狀態(tài)定義,3,初始狀態(tài),第一次開啟時(shí)的狀態(tài),,電梯的初始狀態(tài),,,表示：當(dāng)系統(tǒng)首次開啟時(shí),pushed,集為空，即所有的按鈕都處于關(guān)閉狀態(tài)。,4,操作,Z語(yǔ)言語(yǔ)法規(guī)定，當(dāng)一個(gè)格被,用在另一個(gè)格中時(shí)，要在它的前面加上一個(gè)三角形符號(hào),,電梯的例子,,△,4,操作,電梯例子，到達(dá)樓層,,△,4.4.2,評(píng)價(jià),Z語(yǔ)言成功的原因：,,(1)容易發(fā)現(xiàn)用Z寫的規(guī)格說(shuō)明的錯(cuò)誤,,(2)用Z寫規(guī)格說(shuō)明時(shí)，要十分精確地使用Z說(shuō)明符，減少了不一致性和遺漏。,,(3)可以嚴(yán)格地驗(yàn)證說(shuō)明的正確性。,,(4)學(xué)會(huì)編寫Z規(guī)格說(shuō)明比較容易,,(5)減少開發(fā)總時(shí)間，減少費(fèi)用,,(6)可以用自然語(yǔ)言重寫規(guī)格說(shuō)明，說(shuō)明更清楚，更正確。,