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

《軟件工程導論class5形式化說明技術(shù)》由會員分享，可在線閱讀，更多相關(guān)《軟件工程導論class5形式化說明技術(shù)（43頁珍藏版）》請在裝配圖網(wǎng)上搜索。

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

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

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

4、法顧問隨時提供咨詢,,絕大多數(shù)軟件工程師對形式化方法中使用的數(shù)學和邏輯 并不很熟悉，而且沒受過使用形式化方法的專業(yè)訓練,,需要專家指導和培訓,,,4.1.3,應用形式化方法的準則,(5),不應該放棄傳統(tǒng)的開發(fā)方法,,形式化方法和結(jié)構(gòu)化方法或面向?qū)ο蠓椒善饋砜赡?取長補短,,(6),應該建立詳盡的文檔,,使用自然語言注釋形式化的規(guī)格說明書，以幫助用戶和 維護人員理解系統(tǒng),,,4.1.3,應用形式化方法的準則,(7),不應該放棄質(zhì)量標準,,形式化方法僅僅有助于開發(fā)出高質(zhì)量軟件的一種手段,,,系統(tǒng)開發(fā)過程中仍然必須一如既往地實施其他質(zhì)量保證活動,,(8),不應該盲目依賴形式化方法,,形式化方法并

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

6、，分別標記為,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:,由當前狀態(tài)和當前輸入確定下一個狀態(tài),(,次態(tài),),,初始態(tài),S,,終態(tài)集,F,,,?,,4.2.1,概念,有窮狀態(tài)機可以表示為一個,5,元組,(J,，,K,，,T,，,

7、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)機的應用,,每個菜單驅(qū)動的用戶界面,:,一個菜單的顯示和一個狀態(tài)相對應，鍵盤輸入或

8、用鼠標選擇一個圖標是使系統(tǒng)進入其他狀態(tài) 的一個事件,,狀態(tài)的每個轉(zhuǎn)換都具有下面的形式：,,當前狀態(tài),〔,菜單,〕,+,事件,〔,所選擇的項,〕 →,下個狀態(tài)。,,當前狀態(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)需

9、求,,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ù),,,用于解決如同步問題、競爭條件以及死鎖問題等問題,,應用領(lǐng)域,,自動化,,性能評價,,操作系統(tǒng),,軟件工程 有效地描述,并發(fā)活動,,,,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,｝是一個有窮位置集，,n,≥,0,。,,T=,｛,t1,，,…,，,tm,｝是一個有窮轉(zhuǎn)換集，,m,≥,0,，且,T,和,P,不相交。,,I,：,T,→,P,∞為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組,(bags),的映射。

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

12、tri,網(wǎng)是一組位置到一向量的映射,,M：P→{0,1，2，…},,帶有標記的,Petri,網(wǎng)成為一個,5元組,,(P，T，I，O，M),4.3.1,概念,對,Petri,網(wǎng)的一個重要擴充是加入禁止線，禁止線用一個小圓圈標記輸入線。當輸入線上至少有一個權(quán)標，而禁止線上沒有權(quán)標時，相應的轉(zhuǎn)換才是允許的。如圖,4.9,，,P,3,上有一個權(quán)標而P,2,上沒有，,,因此轉(zhuǎn)換t,1,可以激發(fā)。,4.3.2,例子,F,f,表示樓層，電梯用權(quán)標代表，在位置,F,f,有,權(quán)標,，表示在,樓層,f,上有電梯,。,,電梯中樓層,f的按鈕，用位置EB,f,表示。在,EB,f,,上有一個,權(quán)標,，表示,電梯內(nèi)樓層,

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

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