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