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

,單擊此處編輯母版標(biāo)題樣式,單擊此處編輯母版文本樣式,第二級,第三級,第四級,第五級,*,*,*,第4章 形式化說明技術(shù),4.1 概述,4.2 有窮狀態(tài)機(jī),4.3 Petri網(wǎng),4.4 Z語言,4.5 小結(jié),1,關(guān)于形式化方法,形式化方法是有爭議的。它們的支持者宣稱：它們可以引發(fā)軟件開發(fā)的革命。而批評者認(rèn)為：這是困難和不可能的。同時，對于大多數(shù)人來說，對形式化方法是如此不熟悉，以至難于判斷這些爭論。,2,形式化的程序,非形式化方法：自然語言描述,半形式化方法（欠形式化方法）：數(shù)據(jù)流圖、實體-聯(lián)系圖,形式化方法：一種方法有堅實的數(shù)學(xué)基礎(chǔ),3,非形式化方法的缺點(diǎn),二義性：操作員名和口令,可能存在矛盾：監(jiān)控溫度/往往距離很遠(yuǎn),含糊性：由雷達(dá)操作員使用的系統(tǒng)界面應(yīng)該是用戶友好的,不完整性：傳感器,抽象層次混亂：系統(tǒng)的目的是跟蹤倉庫中的庫存/當(dāng)?shù)陠T輸入命令withdraw及參數(shù)，系統(tǒng)將回饋是否允許移去貨物,4,形式化方法的優(yōu)點(diǎn),簡潔,幾乎可以沒有二義性,可以通過數(shù)學(xué)方法來發(fā)現(xiàn)矛盾和不完整性,在不同軟件工程活動之間平滑地過渡,提供了高層確認(rèn)的手段,5,有窮狀態(tài)機(jī),有窮狀態(tài)機(jī)：可以準(zhǔn)確的描述一個系統(tǒng),6,有窮狀態(tài)機(jī),有窮狀態(tài)機(jī)的組成部分（五元組）,狀態(tài)集,輸入集,轉(zhuǎn)換函數(shù),初始態(tài),終態(tài)集,7,有窮狀態(tài)機(jī),謂詞：全局狀態(tài)的函數(shù),“貓是動物”一句中的“是動物”就是一個謂詞，而“貓”是客體,“3大于2”中“大于”是一個謂詞,轉(zhuǎn)換規(guī)則：,當(dāng)前狀態(tài)菜單+事件所選擇的項=下個狀態(tài),當(dāng)前狀態(tài)菜單+事件所選擇的項+謂詞=下個狀態(tài),8,有窮狀態(tài)機(jī),電梯系統(tǒng)的描述,9,有窮狀態(tài)機(jī),10,有窮狀態(tài)機(jī),便于書寫，驗證,可以通過CASE工具將有窮狀態(tài)機(jī)的規(guī)格說明直接轉(zhuǎn)變?yōu)樵创a,開發(fā)一個規(guī)模比較大的系統(tǒng)時，三元組數(shù)量太多,沒有處理定時需求,11,Petri網(wǎng),Petri網(wǎng)：最初用于自動化處理方面，后來才用于計算機(jī)科學(xué)中,位置：用圓圈表示,轉(zhuǎn)換：用短直線表示,用于轉(zhuǎn)換的輸入函數(shù)：由位置指向轉(zhuǎn)換的箭頭表示,用于轉(zhuǎn)換的輸出函數(shù)：由轉(zhuǎn)換指向位置的箭頭表示,12,Petri網(wǎng),權(quán)標(biāo)（Token）及權(quán)標(biāo)的表示,帶權(quán)標(biāo)的Petri網(wǎng)：是否允許轉(zhuǎn)換,禁止線：帶小圓圈的輸入線表示,帶禁止線的Petri網(wǎng),13,Petri網(wǎng),14,Petri網(wǎng),15,Z語言,Z語言包含的內(nèi)容：,給定的集合、數(shù)據(jù)類型及常數(shù),狀態(tài)定義,初始狀態(tài),操作,16,Z語言,給定的集合：用表示,狀態(tài)定義：格（schema）,初始狀態(tài),操作：？表示輸入變量，！表示輸出變量，表示某個變量的值發(fā)生了改變，表示差運(yùn)算,17,Z語言,18,Z語言,19,Z語言,20,Z語言,塊處理,21,Z語言,22,Z語言,23,Z語言,24,Z語言,用Z語言書寫的規(guī)格說明，比較容易發(fā)現(xiàn)錯誤,減少了模糊性、不一致性和遺漏,可以嚴(yán)格驗證規(guī)格說明的正確性,雖然完全掌握Z語言困難，但是學(xué)會編寫還是比較容易的,使用Z語言可以降低軟件開發(fā)費(fèi)用和總時間,從Z語言的規(guī)格說明轉(zhuǎn)換出自然語言的規(guī)格說明更為清晰,25,應(yīng)用形式化方法的準(zhǔn)則,應(yīng)該選用適當(dāng)?shù)谋硎痉椒?應(yīng)該形式化，但不要過分形式化,應(yīng)該估算成本,應(yīng)該有形式化方法顧問隨時提供咨詢,不應(yīng)該放棄傳統(tǒng)的開發(fā)方法,應(yīng)該建立詳盡的文檔,不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn),不應(yīng)該盲目依賴形式化方法,應(yīng)該測試、測試再測試,應(yīng)該重用,26,形式化方法的未來發(fā)展,目前還沒有在業(yè)界廣泛應(yīng)用,形式化技術(shù)主要關(guān)注于功能和數(shù)據(jù)，而問題的時序、控制和行為等方面卻更難于表達(dá),有些問題元素（界面）也最好用圖形技術(shù)來刻畫,形式化技術(shù)學(xué)習(xí)起來相對困難,很有可能成為新一代CASE工具的基礎(chǔ),27,本章小結(jié),非形式化方法的缺點(diǎn),形式化方法的優(yōu)點(diǎn),有限狀態(tài)機(jī),Petri網(wǎng),Z語言,形式化方法的未來發(fā)展,28,