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

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