第1章 軟件及其開發(fā)概述

1、1軟件開發(fā)的形式化方法 Formal Methods for Software Development （軟件工程中的形式化方法）杜玉越 2參考資料o 古天龍，軟件開發(fā)的形式化方法，高等教育出版社，2005o Alagar V.S. and Periyasamy K., Specification of Software Systems, Springer-Verlag, New York, 1998o Clark E. and Wing J., Formal Methods: State of the Art and Future Direction. CMU-CS-96-178, CMU

2、Computer Science Technical Report, 1996, 1-22 3課程的主要任務(wù)(W2H)o W(Why) 為什么要學(xué)習(xí)形式化方法?o W(What)形式化方法的基本原理是什么?o H(How) 如何將形式化方法集成到軟件開發(fā)過程?4掌握內(nèi)容o 軟件開發(fā)中形式化的必要性o 形式化方法的數(shù)學(xué)基礎(chǔ)o 典型形式化方法及語言o 形式化方法在軟件開發(fā)中的應(yīng)用5課程安排o 概述o 有限狀態(tài)機(jī)及其擴(kuò)展o Petri網(wǎng)o 進(jìn)程代數(shù)o Pi演算o 時(shí)態(tài)邏輯o 動態(tài)描述邏輯6Chapter 1 軟件及其開發(fā)軟件及其開發(fā)概述概述 o 1.1 軟件開發(fā)的歷史軟件開發(fā)的歷史o 1.2 軟件危

3、機(jī)軟件危機(jī)o 1.3 軟件工程軟件工程o 1.4 形式化方法形式化方法 71.1 軟件開發(fā)的歷史軟件開發(fā)的歷史o 軟件是與硬件相互依存，與硬件合為一體完成計(jì)算機(jī)系統(tǒng)功能o 1946-1964：軟件費(fèi)用占20%o 1965-1980: 軟件費(fèi)用占60%o 1981-至今： 軟件費(fèi)用持續(xù)上升，現(xiàn)在已達(dá)80%以上81.1 軟件開發(fā)的歷史軟件開發(fā)的歷史o 軟件開發(fā)：把現(xiàn)實(shí)世界的需求反映成軟件模型，并予以實(shí)現(xiàn)的過程o 軟件及其開發(fā)經(jīng)歷了三個(gè)階段o 第一階段：程序設(shè)計(jì)階段（1946-1956）n從第一臺電子數(shù)字計(jì)算機(jī)ENIAC誕生，到高級語言的出現(xiàn)n計(jì)算機(jī)用于科學(xué)計(jì)算與工程計(jì)算，處理對像是數(shù)值數(shù)據(jù)n個(gè)體手

4、工編程，編程工具：匯編語言和機(jī)器語言n“軟件”一詞尚未出現(xiàn)9第二階段：程序系統(tǒng)階段（1956-1968）o 1956年J.Backus（美）研制的FORTRAN語言問世，高級語言的誕生o 應(yīng)用領(lǐng)域：涉及到非數(shù)值數(shù)據(jù)、數(shù)據(jù)處理o 編程工具：高級語言o 此時(shí)的“軟件”指程序及其說明書o 開發(fā)周期變長，出現(xiàn)了“軟件危機(jī)”o 正確性、可靠性受到關(guān)注10第三階段：軟件工程階段（1968-）o 1968年在德國北大西洋公約組織北大西洋公約組織 (North Atlantic Treaty Organisation-NATO)召開的軟件危機(jī)問題的會議上，提出了“軟件工程”的概念o 軟件應(yīng)用領(lǐng)域急劇擴(kuò)大，有一

5、個(gè)龐大的市場用戶群體o 軟件開發(fā)方式轉(zhuǎn)向工程方式o 軟件開發(fā)除高級語言外，還有需求定義語言、軟件設(shè)計(jì)語言等o 出現(xiàn)了面向?qū)ο?、網(wǎng)絡(luò)及分布式開發(fā)等技術(shù)111.2 軟件危機(jī)o 軟件危機(jī)（Software Crisis）n 在計(jì)算機(jī)軟件的開發(fā)和維護(hù)過程中所遇到的一系列嚴(yán)重問題n 1968年在德國北大西洋公約組織北大西洋公約組織NATO召開的召開的國際會議上提出國際會議上提出o 包含兩個(gè)方面問題包含兩個(gè)方面問題n 如何開發(fā)軟件，才能滿足不斷增長、日趨復(fù)雜如何開發(fā)軟件，才能滿足不斷增長、日趨復(fù)雜的需求的需求n 如何維護(hù)數(shù)量不斷膨脹的軟件產(chǎn)品如何維護(hù)數(shù)量不斷膨脹的軟件產(chǎn)品121.2 軟件危機(jī)o 主要表現(xiàn)n

6、 開發(fā)成本昂貴開發(fā)成本昂貴n 項(xiàng)目進(jìn)度難控項(xiàng)目進(jìn)度難控n 質(zhì)量無法保證質(zhì)量無法保證n 修改維護(hù)困難修改維護(hù)困難13 開發(fā)成本昂貴開發(fā)成本昂貴軟件成本日益增長（軟件成本日益增長（1）o 1968年，美國花費(fèi)于軟件的投資高達(dá)60億美元，有些系統(tǒng)，特別是軍用系統(tǒng)，軟件費(fèi)用要高出硬件費(fèi)用好幾倍，例如美國全球軍事指揮控制系統(tǒng)的計(jì)算機(jī)硬件費(fèi)用為1億美元，而軟件費(fèi)用高達(dá)7.2億美元。o 1980年美國政府的財(cái)政年度當(dāng)中，計(jì)算機(jī)系統(tǒng)方面(軟，硬件與服務(wù))共耗資達(dá)570億美元，其中320億美元(占總數(shù)的56)用于計(jì)算機(jī)軟件方面(與同年的美國汽車行業(yè)進(jìn)行簡單的比較，美國是當(dāng)時(shí)的世界第一汽車生產(chǎn)大國，汽車的年銷售量

7、為900萬輛，總的銷售額僅為720億美元。14 開發(fā)成本昂貴開發(fā)成本昂貴軟件成本日益增長（軟件成本日益增長（2）o 技術(shù)的進(jìn)步使得計(jì)算機(jī)硬件的成本持續(xù)降低，而軟件成本則不斷增長，軟件成本在計(jì)算機(jī)系統(tǒng)總成本中所占的比例呈現(xiàn)日益擴(kuò)大的趨勢o 美國空軍計(jì)算機(jī)系統(tǒng)的數(shù)據(jù)表明，1970年，軟件費(fèi)用約占總費(fèi)用的60，1975年達(dá)到72，1980年達(dá)到80，1985年計(jì)達(dá)到85。（1979年，美國的國防預(yù)算為1258億美元，其中9%用于計(jì)算機(jī)領(lǐng)域，約113億美元。在這113億美元當(dāng)中，91億美元（約占80）用于軟件投資。15 項(xiàng)目進(jìn)度難控項(xiàng)目進(jìn)度難控o 為軟件開發(fā)制定進(jìn)度是很困難的事情o 通常根據(jù)其復(fù)雜性、

8、工作量及進(jìn)度要求安排人力。o 軟件開發(fā)不同于傳統(tǒng)的機(jī)械制造，人多不見得軟件開發(fā)不同于傳統(tǒng)的機(jī)械制造，人多不見得力量大力量大。o 如果給落后于計(jì)劃的項(xiàng)目增添新人，可能會更加延誤項(xiàng)目。16 項(xiàng)目進(jìn)度難控項(xiàng)目進(jìn)度難控o 1998年，美國企業(yè)應(yīng)用項(xiàng)目不成功率高達(dá)75%，其中28%的項(xiàng)目最終被取消，40%的項(xiàng)目周期被無限拖長或資金超出預(yù)算。p Brook提出的法則“在已拖延的軟件項(xiàng)目上增加在已拖延的軟件項(xiàng)目上增加人力只會使其更難按期完成人力只會使其更難按期完成” 。17 質(zhì)量無法保證質(zhì)量無法保證 o 1985年11月21日,由于計(jì)算機(jī)軟件的錯(cuò)誤,造成紐約紐約銀行與美聯(lián)儲電子結(jié)算系統(tǒng)銀行與美聯(lián)儲電子結(jié)算系

9、統(tǒng)收支失衡,發(fā)生了超額支付,而這個(gè)問題一直到晚上才被發(fā)現(xiàn),紐約銀行當(dāng)日帳務(wù)出現(xiàn)了出現(xiàn)了230億億的短款。o Therac-25是加拿大原子能公司AECL和一家法國公司CGR聯(lián)合開發(fā)的一種醫(yī)療設(shè)備，它產(chǎn)生的高能光束或電子流能夠殺死人體毒瘤而不會傷害毒瘤附近的人體健康組織。該設(shè)備于1982年正式投入生產(chǎn)和使用，在1985年6月到1987年1月的不到兩年的時(shí)間里，因?yàn)檐浖毕菀l(fā)了因?yàn)檐浖毕菀l(fā)了6起由于電子流或起由于電子流或X-光束的光束的過量使用的醫(yī)療事故，造成過量使用的醫(yī)療事故，造成4人死亡、人死亡、2人重傷的嚴(yán)人重傷的嚴(yán)重后果重后果。18 質(zhì)量無法保證（續(xù)）質(zhì)量無法保證（續(xù)）o1996年，

10、歐洲航天局阿麗亞娜阿麗亞娜5型（型（Ariane5）火箭火箭在發(fā)射后40秒鐘后發(fā)生爆炸，發(fā)射基地上2名法國士兵當(dāng)場死亡，損耗資產(chǎn)達(dá)10億美元之巨，歷時(shí)9年的航天計(jì)劃因此嚴(yán)重受挫。事后專家的調(diào)查分析報(bào)告指出，爆炸原因在于慣性導(dǎo)航系統(tǒng)軟爆炸原因在于慣性導(dǎo)航系統(tǒng)軟件技術(shù)要求和設(shè)計(jì)的錯(cuò)誤件技術(shù)要求和設(shè)計(jì)的錯(cuò)誤。 o2002年，美國商務(wù)部的國立標(biāo)準(zhǔn)技術(shù)研究所（NIST）發(fā)表了一個(gè)有關(guān)軟件缺陷的損失的調(diào)查報(bào)告。該報(bào)告表示：“據(jù)推測，據(jù)推測，由于軟件缺陷而引起的損失額每年高達(dá)由于軟件缺陷而引起的損失額每年高達(dá)595億美元。這一數(shù)字億美元。這一數(shù)字相當(dāng)于美國國內(nèi)生產(chǎn)總值的相當(dāng)于美國國內(nèi)生產(chǎn)總值的0.6%”。對

11、于一些安全悠關(guān)的系對于一些安全悠關(guān)的系統(tǒng)，軟件的缺陷更是造成了災(zāi)難性的后果。統(tǒng)，軟件的缺陷更是造成了災(zāi)難性的后果。o2007年年10月月30日，北京奧運(yùn)門票網(wǎng)上預(yù)訂系統(tǒng)開通首日即日，北京奧運(yùn)門票網(wǎng)上預(yù)訂系統(tǒng)開通首日即遭癱瘓，兩小時(shí)內(nèi)各個(gè)銷售渠道僅售出門票約遭癱瘓，兩小時(shí)內(nèi)各個(gè)銷售渠道僅售出門票約9000張。張。19 修改維護(hù)困難修改維護(hù)困難o 軟件的維護(hù)任務(wù)特別重軟件的維護(hù)任務(wù)特別重o 正式投入使用的商用軟件，總是存在著一定數(shù)量的錯(cuò)誤。o 隨著時(shí)間的延伸，在不同的運(yùn)行條件下，軟件就會出現(xiàn)故障，就需要維護(hù)。o 軟件維護(hù)是要糾正邏輯缺陷o 當(dāng)軟件系統(tǒng)變得龐大，問題變得復(fù)雜時(shí)，常常當(dāng)軟件系統(tǒng)變得龐大

12、，問題變得復(fù)雜時(shí)，常常會發(fā)生會發(fā)生“糾正一個(gè)錯(cuò)誤帶來更多新的錯(cuò)誤！糾正一個(gè)錯(cuò)誤帶來更多新的錯(cuò)誤！”的問題。的問題。 20 軟件危機(jī)的原因軟件危機(jī)的原因o 客觀上客觀上主要表現(xiàn)在：主要表現(xiàn)在：n規(guī)模的復(fù)雜性規(guī)模的復(fù)雜性n結(jié)構(gòu)的復(fù)雜性結(jié)構(gòu)的復(fù)雜性n環(huán)境的復(fù)雜性環(huán)境的復(fù)雜性n領(lǐng)域的復(fù)雜性領(lǐng)域的復(fù)雜性n交流的復(fù)雜性交流的復(fù)雜性 o 主觀上主觀上主要表現(xiàn)在：主要表現(xiàn)在：n缺乏指導(dǎo)或?qū)嵤┸浖O(shè)計(jì)、開發(fā)、維護(hù)的有效理論、方缺乏指導(dǎo)或?qū)嵤┸浖O(shè)計(jì)、開發(fā)、維護(hù)的有效理論、方法及技術(shù)法及技術(shù)nOR 缺乏有效解決軟件設(shè)計(jì)、開發(fā)、維護(hù)中相關(guān)實(shí)際問缺乏有效解決軟件設(shè)計(jì)、開發(fā)、維護(hù)中相關(guān)實(shí)際問題的理論、方法及技術(shù)題的理論

13、、方法及技術(shù) 21 規(guī)模的復(fù)雜性規(guī)模的復(fù)雜性 o 以美國宇航局的軟件系統(tǒng)為例：以美國宇航局的軟件系統(tǒng)為例：19631963年，水星計(jì)劃的軟年，水星計(jì)劃的軟件系統(tǒng)約有件系統(tǒng)約有 200 200萬條指令；萬條指令；19791979年，哥倫比亞航天飛機(jī)年，哥倫比亞航天飛機(jī)系統(tǒng)達(dá)到了系統(tǒng)達(dá)到了40004000萬條指令。萬條指令。o 軟件龐大的規(guī)模是引起技術(shù)上和心理上挫折的一個(gè)重要因素o 在需求分析及生成規(guī)格的階段,由于需要搜集和分析的信息量巨大，從而可能會使得信息不正確或不完整，并且在審查階段也未能檢查出來。o 有人認(rèn)為：幾乎所有與計(jì)算機(jī)過程控制系統(tǒng)有關(guān)的事故幾乎所有與計(jì)算機(jī)過程控制系統(tǒng)有關(guān)的事故都是

14、源于這類由軟件規(guī)模因素所引起的錯(cuò)誤。都是源于這類由軟件規(guī)模因素所引起的錯(cuò)誤。22 結(jié)構(gòu)的復(fù)雜性結(jié)構(gòu)的復(fù)雜性 o 結(jié)構(gòu)復(fù)雜性體現(xiàn)在管理和技術(shù)兩個(gè)方面。o 在管理方面，開發(fā)小組用來組織和管理開發(fā)活動時(shí)所采用的層次的寬度和深度，決定了用來管理系統(tǒng)結(jié)構(gòu)的復(fù)雜性；o 在技術(shù)方面，軟件系統(tǒng)的模塊結(jié)構(gòu)愈加復(fù)雜，模塊之間復(fù)雜的調(diào)用關(guān)系以及接口信息往往超模塊之間復(fù)雜的調(diào)用關(guān)系以及接口信息往往超過了人們所能接受的程度過了人們所能接受的程度。 23 環(huán)境的復(fù)雜性環(huán)境的復(fù)雜性 o 運(yùn)行中的軟件總是受其所處環(huán)境的影響，在接收到外界環(huán)境的觸發(fā)事件時(shí)，軟件應(yīng)該做出正確的響應(yīng)。o 許多系統(tǒng)只有當(dāng)成功地運(yùn)行于其環(huán)境時(shí)，才能對其

15、環(huán)境進(jìn)行很好的理解。o 軟件運(yùn)行環(huán)境的多樣性和異構(gòu)性給軟件開發(fā)者帶來了更大的挑戰(zhàn)。 24 領(lǐng)域的復(fù)雜性領(lǐng)域的復(fù)雜性 o 軟件中所操作的對象僅僅是對應(yīng)用領(lǐng)域真實(shí)對象的模擬o 對于有的應(yīng)用領(lǐng)域來說，這些模擬只能是近似的。其原因可能是由于對應(yīng)用領(lǐng)域?qū)ο蟮恼J(rèn)識不完全，或者是由于該模型所具有的苛刻條件限制，或者兩者兼而有之。o 在某些軟件應(yīng)用領(lǐng)域中，并不存在可以認(rèn)知的模型，或在某些軟件應(yīng)用領(lǐng)域中，并不存在可以認(rèn)知的模型，或者沒有準(zhǔn)確的模型來描繪相應(yīng)的物理對象的幾何、拓?fù)湔邲]有準(zhǔn)確的模型來描繪相應(yīng)的物理對象的幾何、拓?fù)湟约捌渌卣饕约捌渌卣鳌 在這種缺少準(zhǔn)確認(rèn)識的情況下，應(yīng)用領(lǐng)域的某些方面很可能在軟件

16、中不能體現(xiàn)出來。25 交流的復(fù)雜性交流的復(fù)雜性 o 團(tuán)隊(duì)里的每個(gè)人參與開發(fā)過程中的一個(gè)或多個(gè)活動。o 對于參與不同開發(fā)階段的人來說，彼此之間明確的交流非常重要。o 成員間交流時(shí)使用的媒介往往是自然語言、圖、表等非形式化的方式，它們很難準(zhǔn)確地描述所開發(fā)產(chǎn)品的基本屬性。o 這些媒介本身具有二義性，往往會使開發(fā)人員產(chǎn)生錯(cuò)誤的理解，這種錯(cuò)誤將會隨著開發(fā)過程的進(jìn)行而逐漸蔓延開來，最終導(dǎo)致災(zāi)難性的后果。 26軟件危機(jī)解決方案o 一類是一類是采用工程的方法來組織和管理軟件的采用工程的方法來組織和管理軟件的開發(fā)，這導(dǎo)致了開發(fā)，這導(dǎo)致了軟件工程軟件工程的產(chǎn)生和發(fā)展。的產(chǎn)生和發(fā)展。o 一類是從理論上探討程序正確性

17、和軟件可靠從理論上探討程序正確性和軟件可靠性、可信性問題，這推動了性、可信性問題，這推動了軟件形式化技術(shù)軟件形式化技術(shù)的研究的研究271.31.3 軟件工程軟件工程 工程化的軟件開發(fā)工程化的軟件開發(fā) （類似于建筑、汽車、機(jī)械等其它行業(yè)）（類似于建筑、汽車、機(jī)械等其它行業(yè)） 設(shè)計(jì)、生產(chǎn)、維護(hù)的規(guī)范化及科學(xué)化設(shè)計(jì)、生產(chǎn)、維護(hù)的規(guī)范化及科學(xué)化 不規(guī)范不規(guī)范規(guī)范；非嚴(yán)格規(guī)范；非嚴(yán)格嚴(yán)格；非形式嚴(yán)格；非形式形式；形式； 無方法無方法/ /技術(shù)技術(shù)方法方法/ /技術(shù)技術(shù) 尋求工程化的軟件開發(fā)的原理、方法及技術(shù)尋求工程化的軟件開發(fā)的原理、方法及技術(shù)281.3 1.3 軟件工程軟件工程 o19831983年年

18、IEEEIEEE給軟件工程下的定義是：給軟件工程下的定義是：“軟件工程是開發(fā)、運(yùn)行、維護(hù)和軟件工程是開發(fā)、運(yùn)行、維護(hù)和修復(fù)軟件的系統(tǒng)方法修復(fù)軟件的系統(tǒng)方法”這個(gè)定義相當(dāng)概括，它主要強(qiáng)調(diào)軟件工程是系統(tǒng)這個(gè)定義相當(dāng)概括，它主要強(qiáng)調(diào)軟件工程是系統(tǒng)方法而不是某種神秘的個(gè)人技巧。方法而不是某種神秘的個(gè)人技巧。 oFairlyFairly認(rèn)為：認(rèn)為：“軟件工程學(xué)是為了在成本限額以內(nèi)按時(shí)完成開發(fā)和修改軟件工程學(xué)是為了在成本限額以內(nèi)按時(shí)完成開發(fā)和修改軟件產(chǎn)品所需要的系統(tǒng)生產(chǎn)和維護(hù)技術(shù)及管理學(xué)科。軟件產(chǎn)品所需要的系統(tǒng)生產(chǎn)和維護(hù)技術(shù)及管理學(xué)科?！边@個(gè)定義明確指這個(gè)定義明確指出了軟件工程的目標(biāo)是在成本限額內(nèi)按時(shí)完成

19、開發(fā)和修改軟件的工作，出了軟件工程的目標(biāo)是在成本限額內(nèi)按時(shí)完成開發(fā)和修改軟件的工作，同時(shí)也指出了軟件工程包含技術(shù)和管理兩方而的內(nèi)容。同時(shí)也指出了軟件工程包含技術(shù)和管理兩方而的內(nèi)容。 oFritz BauerFritz Bauer給出了下述定義：給出了下述定義：“軟件工程是為了經(jīng)濟(jì)地獲得可靠的且能軟件工程是為了經(jīng)濟(jì)地獲得可靠的且能在實(shí)際機(jī)器上有效運(yùn)行的軟件，而建立和使用的完善的工程化原則。在實(shí)際機(jī)器上有效運(yùn)行的軟件，而建立和使用的完善的工程化原則?！边@個(gè)定義不僅指出軟件工程的目標(biāo)是經(jīng)濟(jì)地開發(fā)出高質(zhì)量的軟什，而且這個(gè)定義不僅指出軟件工程的目標(biāo)是經(jīng)濟(jì)地開發(fā)出高質(zhì)量的軟什，而且強(qiáng)調(diào)了軟件工程是一門工程

20、學(xué)科，它應(yīng)該建立并使用完善的工程化原則。強(qiáng)調(diào)了軟件工程是一門工程學(xué)科，它應(yīng)該建立并使用完善的工程化原則。o19931993年年IEEEIEEE進(jìn)一步給出了一個(gè)更全面的定義進(jìn)一步給出了一個(gè)更全面的定義“軟件上程是：軟件上程是： 把系統(tǒng)化把系統(tǒng)化的、規(guī)范的、可度量的途徑應(yīng)用于軟件并發(fā)、運(yùn)行和維護(hù)的過程，也就的、規(guī)范的、可度量的途徑應(yīng)用于軟件并發(fā)、運(yùn)行和維護(hù)的過程，也就是把工程化應(yīng)用于軟件中；是把工程化應(yīng)用于軟件中； 研究中提到的途徑。研究中提到的途徑?！?9軟件工程三要素o 方法：提供如何構(gòu)造軟件的技術(shù)，是完成軟件工程項(xiàng)目的技術(shù)手段；o 工具：為軟件工程方法提供自動化或半自動化的支持；o 過程：將

21、軟件工程的方法和工具綜合起來以達(dá)到合理、及時(shí)地進(jìn)行計(jì)算機(jī)軟件開發(fā)的目的。30軟件工程的主要內(nèi)容o 軟件工程過程o 軟件生存周期o 軟件開發(fā)模型o 軟件開發(fā)方法o 軟件工具o 軟件開發(fā)環(huán)境o 計(jì)算機(jī)輔助軟件工程o 軟件工程經(jīng)濟(jì)學(xué)31 軟件工程過程o 規(guī)定獲取、供應(yīng)、開發(fā)、操作及維護(hù)軟件時(shí)，所需實(shí)施的過程、活動和任務(wù)。o 為各類人員提供一個(gè)公共的框架，以便用相同的語言進(jìn)行交流。o 軟件工程過程包括開發(fā)過程、管理過程、供軟件工程過程包括開發(fā)過程、管理過程、供應(yīng)過程、獲取過程、操作過程、維護(hù)過程及應(yīng)過程、獲取過程、操作過程、維護(hù)過程及支持過程。支持過程。32 軟件生命周期o 與軟件產(chǎn)品相關(guān)的一系列活動

22、的全周期，包括如下與軟件產(chǎn)品相關(guān)的一系列活動的全周期，包括如下五個(gè)活動五個(gè)活動：o 需求分析和規(guī)格：需求分析，邏輯模型，需求規(guī)格；o 軟件設(shè)計(jì)：總體結(jié)構(gòu)設(shè)計(jì)，具體模塊實(shí)現(xiàn)算法設(shè)計(jì)；o 程序編寫：軟件設(shè)計(jì)結(jié)果的編程實(shí)現(xiàn)；o 軟件測試：模塊測試，組裝測試，確認(rèn)測試；o 運(yùn)行和維護(hù)：軟件的維護(hù)與修改，時(shí)間最長、工作量最大、費(fèi)用最高的一項(xiàng)活動。33 軟件開發(fā)模型（軟件生命周期模型）o 指從軟件項(xiàng)目需求定義開始，直至軟件被淘汰，跨指從軟件項(xiàng)目需求定義開始，直至軟件被淘汰，跨越整個(gè)生存期的系統(tǒng)開發(fā)、運(yùn)行和維護(hù)所實(shí)施的全越整個(gè)生存期的系統(tǒng)開發(fā)、運(yùn)行和維護(hù)所實(shí)施的全部過程、活動和任務(wù)的結(jié)構(gòu)框架。部過程、活動和

23、任務(wù)的結(jié)構(gòu)框架。o 確立了軟件開發(fā)各階段的次序及任務(wù)和活動準(zhǔn)則，給出了開發(fā)過程中所遵守的規(guī)定和限制。o 主要軟件開發(fā)模型：瀑布模型瀑布模型（Waterfall Model）、原型模型原型模型（Prototype Model）、螺旋螺旋模型模型（Spiral Model）、構(gòu)件模型構(gòu)件模型（Component Model）、四代技術(shù)模型四代技術(shù)模型（4GT Model）、變換變換模型模型（Transformational Model）34 軟件開發(fā)方法o 指在某種思想指導(dǎo)下，使用已定義的一系列技術(shù)和表示工具，組織軟件開發(fā)過程的方法。o 通常表述為一系列的步驟，每一步驟都與相應(yīng)的技術(shù)和表示工具相關(guān)

24、。o 目的是有效地得到一個(gè)運(yùn)行系統(tǒng)及其支持文檔，并滿足有關(guān)的質(zhì)量要求。o 典型的傳統(tǒng)軟件開發(fā)方法：結(jié)構(gòu)化方法、面向數(shù)據(jù)結(jié)構(gòu)方法、面向?qū)ο蠓椒ǖ取?5 軟件工具o 指用來輔助軟件開發(fā)、維護(hù)和管理的一系列軟件。o 可以節(jié)省開發(fā)時(shí)間和費(fèi)用，提高軟件生產(chǎn)率和軟件質(zhì)量。o 從軟件過程的觀點(diǎn)有：項(xiàng)目管理工具、配置從軟件過程的觀點(diǎn)有：項(xiàng)目管理工具、配置管理工具、分析和設(shè)計(jì)工具、編碼工具、測管理工具、分析和設(shè)計(jì)工具、編碼工具、測試工具、維護(hù)工具等試工具、維護(hù)工具等。36 軟件開發(fā)環(huán)境o 支持軟件產(chǎn)品生產(chǎn)的軟件系統(tǒng)，由軟件工具支持軟件產(chǎn)品生產(chǎn)的軟件系統(tǒng)，由軟件工具和集成機(jī)制組成和集成機(jī)制組成。o 軟件工具用于支

25、持軟件開發(fā)的相關(guān)過程、活動和任務(wù)o 集成機(jī)制為工具集成和軟件的開發(fā)、管理和維護(hù)，提供統(tǒng)一的支持37 計(jì)算機(jī)輔助軟件工程o 旨在實(shí)現(xiàn)軟件生命周期各個(gè)環(huán)節(jié)的自動化并旨在實(shí)現(xiàn)軟件生命周期各個(gè)環(huán)節(jié)的自動化并使之成為一個(gè)整體使之成為一個(gè)整體o 計(jì)算機(jī)輔助軟件工程技術(shù)是軟件工具和軟件開發(fā)方法的結(jié)合o 它強(qiáng)調(diào)解決整個(gè)軟件開發(fā)過程的效率問題，而不是解決個(gè)別階段的問題o 它著眼于軟件分析、設(shè)計(jì)和實(shí)現(xiàn)的自動化o 使用圖形功能對軟件系統(tǒng)進(jìn)行說明并建立文檔38 軟件工程經(jīng)濟(jì)學(xué)o 旨在從經(jīng)濟(jì)學(xué)的觀點(diǎn)，研究、分析如何有效旨在從經(jīng)濟(jì)學(xué)的觀點(diǎn)，研究、分析如何有效地開發(fā)、發(fā)布軟件產(chǎn)品和支持用戶使用。地開發(fā)、發(fā)布軟件產(chǎn)品和支持用

26、戶使用。o 研究的問題：成本估算技術(shù)與成本估算模型的建立和使用、軟件工程中不同決策的成本-效益分析、多目標(biāo)決策分析、不確定性的處理和風(fēng)險(xiǎn)分析、工程估計(jì)和控制等。391.41.4 形式化方法形式化方法 （1）o 形式化方法是滲透在軟件生命期中各個(gè)環(huán)節(jié)（如：需形式化方法是滲透在軟件生命期中各個(gè)環(huán)節(jié)（如：需求、設(shè)計(jì)、實(shí)現(xiàn)、測試等）的數(shù)學(xué)方法，求、設(shè)計(jì)、實(shí)現(xiàn)、測試等）的數(shù)學(xué)方法， 或者或者 具有具有嚴(yán)格數(shù)學(xué)基礎(chǔ)的軟件開發(fā)方法嚴(yán)格數(shù)學(xué)基礎(chǔ)的軟件開發(fā)方法o 形式化方法的基本含義是借助數(shù)學(xué)的方法來研究計(jì)算形式化方法的基本含義是借助數(shù)學(xué)的方法來研究計(jì)算機(jī)科學(xué)中的有關(guān)問題。機(jī)科學(xué)中的有關(guān)問題。o Encyclo

27、pedia of Software EngineeringEncyclopedia of Software Engineering對形式對形式化方法定義為：化方法定義為：“用于開發(fā)計(jì)算用于開發(fā)計(jì)算機(jī)系統(tǒng)的形式化方法機(jī)系統(tǒng)的形式化方法是基于數(shù)學(xué)的用于描述系統(tǒng)性質(zhì)的技術(shù)。這樣的形式是基于數(shù)學(xué)的用于描述系統(tǒng)性質(zhì)的技術(shù)。這樣的形式化方法提供了一個(gè)框架，人們可以在該框架中以系統(tǒng)化方法提供了一個(gè)框架，人們可以在該框架中以系統(tǒng)的方式刻畫、開發(fā)和驗(yàn)證系統(tǒng)的方式刻畫、開發(fā)和驗(yàn)證系統(tǒng)”。 o 在軟件開發(fā)的全過程中，凡是采用嚴(yán)格的數(shù)學(xué)語言，在軟件開發(fā)的全過程中，凡是采用嚴(yán)格的數(shù)學(xué)語言，具有精確的數(shù)學(xué)語義的方法，都稱

28、為形式化方法。具有精確的數(shù)學(xué)語義的方法，都稱為形式化方法。401.41.4 形式化方法形式化方法（2 2）o 從廣義角度，從廣義角度，形式化方法是軟件開發(fā)過程中分析、形式化方法是軟件開發(fā)過程中分析、設(shè)計(jì)及實(shí)現(xiàn)的系統(tǒng)工程方法設(shè)計(jì)及實(shí)現(xiàn)的系統(tǒng)工程方法。o 狹義地，狹義地，形式化方法是軟件規(guī)格（形式化方法是軟件規(guī)格（specification）和驗(yàn)證（和驗(yàn)證（verification）的方法。的方法。o 形式化方法又分為形式化規(guī)格方法和形式化驗(yàn)證方形式化方法又分為形式化規(guī)格方法和形式化驗(yàn)證方法。法。o 形式化規(guī)格形式化規(guī)格是通過具有明確數(shù)學(xué)定義的文法和語義是通過具有明確數(shù)學(xué)定義的文法和語義的方法或語

29、言，對軟件的期望特性或者行為進(jìn)行的的方法或語言，對軟件的期望特性或者行為進(jìn)行的精確、簡潔描述。精確、簡潔描述。o 形式化驗(yàn)證形式化驗(yàn)證是基于已建立的形式化規(guī)格，對軟件的是基于已建立的形式化規(guī)格，對軟件的相關(guān)特性進(jìn)行評價(jià)的數(shù)學(xué)分析和證明。相關(guān)特性進(jìn)行評價(jià)的數(shù)學(xué)分析和證明。411.4 1.4 形式化方法形式化方法 （3）o主要目的是保證軟件的正確性。主要目的是保證軟件的正確性。o形式化方法基于嚴(yán)格的數(shù)學(xué)，能夠?qū)ΜF(xiàn)象、對象、動作等進(jìn)行簡潔、形式化方法基于嚴(yán)格的數(shù)學(xué)，能夠?qū)ΜF(xiàn)象、對象、動作等進(jìn)行簡潔、準(zhǔn)確的描述；使得規(guī)格的本質(zhì)可以被展示出來，并且還可以準(zhǔn)確的描述；使得規(guī)格的本質(zhì)可以被展示出來，并且還可

30、以以一種以一種有組織的方式來表示系統(tǒng)規(guī)格中的抽象層次；可使用數(shù)學(xué)證明來揭有組織的方式來表示系統(tǒng)規(guī)格中的抽象層次；可使用數(shù)學(xué)證明來揭示規(guī)格中的矛盾性和不完整性、以及用來展示設(shè)計(jì)和規(guī)格之間的一示規(guī)格中的矛盾性和不完整性、以及用來展示設(shè)計(jì)和規(guī)格之間的一致情況等致情況等。 o2004年年5月，月，IEEE-CS(IEEE-CS(電子電器工程師學(xué)會計(jì)算機(jī)學(xué)會電子電器工程師學(xué)會計(jì)算機(jī)學(xué)會) )和和ACMACM聯(lián)聯(lián)合任合任務(wù)組提交了務(wù)組提交了CCSE（Computing Curriculum-Software Engineering）最終報(bào)告，在該報(bào)告給出的最終報(bào)告，在該報(bào)告給出的SEEK（Software

31、 Engineering Education Knowledge）中，中，“軟件的形式化軟件的形式化方法（方法（Formal Methods in Software Engineering）”被單被單列為一門列為一門必修課程必修課程（序列號為（序列號為SE313）。421.4 1.4 形式化方法形式化方法 （4）o 形式化方法軟件開發(fā)采用了軟件生命周期的形式化方法軟件開發(fā)采用了軟件生命周期的變換模型變換模型, ,就是把現(xiàn)實(shí)世界的需求反映成軟就是把現(xiàn)實(shí)世界的需求反映成軟件的模型化過程。件的模型化過程。o 基于轉(zhuǎn)換模型的軟件開發(fā)（軟件的自動生成）基于轉(zhuǎn)換模型的軟件開發(fā)（軟件的自動生成） o 基于轉(zhuǎn)

32、換模型的軟件基于轉(zhuǎn)換模型的軟件開發(fā)過程實(shí)際上可理解開發(fā)過程實(shí)際上可理解為：為：從最高層的規(guī)格開始，通過一系列的求從最高層的規(guī)格開始，通過一系列的求精變換步驟，每一步都降低一些抽象程度或精變換步驟，每一步都降低一些抽象程度或增加一些可執(zhí)行性，最終得到能夠指導(dǎo)計(jì)算增加一些可執(zhí)行性，最終得到能夠指導(dǎo)計(jì)算機(jī)明確執(zhí)行的程序代碼機(jī)明確執(zhí)行的程序代碼。431.4 1.4 形式化方法形式化方法 （5）o 在進(jìn)行求精的過程中要保證轉(zhuǎn)換之間的一致在進(jìn)行求精的過程中要保證轉(zhuǎn)換之間的一致性和正確性，保證所得到的程序是滿足最初性和正確性，保證所得到的程序是滿足最初規(guī)格的規(guī)格的。o 這種正確性和一致性可以通過求精過程中所

33、這種正確性和一致性可以通過求精過程中所遵循的一系列規(guī)則來保證，也可以在事后采遵循的一系列規(guī)則來保證，也可以在事后采用驗(yàn)證工具來證明。用驗(yàn)證工具來證明。o 基于轉(zhuǎn)換模型的軟件基于轉(zhuǎn)換模型的軟件開發(fā)過程包含了三個(gè)方開發(fā)過程包含了三個(gè)方面的活動：面的活動：形式化規(guī)格、形式化驗(yàn)證、程序形式化規(guī)格、形式化驗(yàn)證、程序求精（求精（refinementrefinement）或變換。或變換。44 形式化規(guī)格形式化規(guī)格o 軟件規(guī)格是指對軟件系統(tǒng)對象及用來對系統(tǒng)對象進(jìn)行操作的方法集合，以及對所開發(fā)系統(tǒng)的各對象在其生存期間的集體行為的描述。o 形式化方法具有嚴(yán)格的語法和語義，可以準(zhǔn)確地描述系統(tǒng)模型，排除矛盾、二義性、

34、含糊性等情況。o 形式規(guī)格精確地描述了用戶的需求、軟件系統(tǒng)的功能及形式規(guī)格精確地描述了用戶的需求、軟件系統(tǒng)的功能及各種性質(zhì)，其描述的是各種性質(zhì)，其描述的是“做什么做什么”，而不考慮，而不考慮“怎么怎么做做”。o 要開發(fā)出良好的規(guī)格，除了應(yīng)透徹理解、熟練掌握所使用的形式規(guī)格語言和方法外，更重要的是對所要描述的系統(tǒng)有全面深入的了解。45 一個(gè)簡單生命周期模型一個(gè)簡單生命周期模型 需求分析系統(tǒng)設(shè)計(jì)I程序開發(fā)軟件測試軟件運(yùn)行BS行行為規(guī)格為規(guī)格 codes代碼實(shí)現(xiàn)代碼實(shí)現(xiàn)PS程程序規(guī)格序規(guī)格DS設(shè)設(shè)計(jì)規(guī)格計(jì)規(guī)格系統(tǒng)設(shè)計(jì)II46 形式化規(guī)格形式化規(guī)格形式化方法可分為三類：操作類、描述類和雙重類。o操作類

35、方法操作類方法：基于狀態(tài)和轉(zhuǎn)移，通過可執(zhí)行模型來描述系統(tǒng)，模型本身能夠采用靜態(tài)分析和模型執(zhí)行而得到驗(yàn)證，這類方法包括有限狀態(tài)機(jī)、Statecharts、Petri網(wǎng)等；o描述類方法描述類方法：基于數(shù)學(xué)公理和概念，通過邏輯或代數(shù)給出系統(tǒng)的狀態(tài)空間，具有高度抽象的特點(diǎn)，便于通過自動工具進(jìn)行驗(yàn)證。有：基于代數(shù)的方法，如Z、VDM、Larch等；以命題線性時(shí)態(tài)邏輯（propositional linear temporal logic，簡稱PLTL）、一階線性時(shí)態(tài)邏輯（first-order linear temporal logic，簡稱FOLTL）、計(jì)算樹邏輯（computation tree t

36、emporal logic，簡稱CTL）等基于邏輯的方法；o雙重類方法雙重類方法：兼有前面二者的特點(diǎn)，既能夠通過數(shù)學(xué)公理和概念來高度抽象地描述系統(tǒng)，又具有狀態(tài)和轉(zhuǎn)移的可執(zhí)行特征，這類方法包括擴(kuò)展?fàn)顟B(tài)機(jī)/實(shí)時(shí)時(shí)態(tài)邏輯（extended state machine / real-time temporal logic，簡稱ESM/RTTL）、TRIO+、TROL等。47 形式化驗(yàn)證形式化驗(yàn)證 o 軟件開發(fā)中的絕大部分錯(cuò)誤是在需求分析和規(guī)格的早期軟件開發(fā)中的絕大部分錯(cuò)誤是在需求分析和規(guī)格的早期階段引入的，這些錯(cuò)誤將隨著開發(fā)的深入而不斷擴(kuò)大，階段引入的，這些錯(cuò)誤將隨著開發(fā)的深入而不斷擴(kuò)大，且發(fā)現(xiàn)的越晚

37、所付出的代價(jià)越大且發(fā)現(xiàn)的越晚所付出的代價(jià)越大。o 傳統(tǒng)的軟件開發(fā)方法中，更多的錯(cuò)誤是到編碼結(jié)束后的測試階段被檢測出來。o 形式化方法中，在開發(fā)出形式規(guī)格后就進(jìn)行形式驗(yàn)證，形式化方法中，在開發(fā)出形式規(guī)格后就進(jìn)行形式驗(yàn)證，使驗(yàn)證工作提前進(jìn)行，早期發(fā)現(xiàn)錯(cuò)誤，減少修改代價(jià)。使驗(yàn)證工作提前進(jìn)行，早期發(fā)現(xiàn)錯(cuò)誤，減少修改代價(jià)。o 形式化驗(yàn)證的主要技術(shù)包括模型檢驗(yàn)和定理證明。o 模型檢驗(yàn)是一種基于有限狀態(tài)模型，并檢驗(yàn)該模型期望特性的技術(shù)。模型檢驗(yàn)主要適用于有窮狀態(tài)系統(tǒng)，完全自動化并且驗(yàn)證速度快。48 形式化驗(yàn)證形式化驗(yàn)證o 模型檢驗(yàn)方法的一個(gè)嚴(yán)重缺陷是“狀態(tài)爆炸”問題。 o 定理證明采用邏輯公式來規(guī)格系統(tǒng)及其

38、性質(zhì)，應(yīng)用公理或推理規(guī)則證明系統(tǒng)具有某些性質(zhì)。o 定理證明可以處理無限狀態(tài)空間問題。o 自動定理證明系統(tǒng)是通用搜索過程，在解決各種組合問題中比較成功o 交互式定理證明系統(tǒng)需要與用戶進(jìn)行交互，要求用戶能提供驗(yàn)證中創(chuàng)造性最強(qiáng)部分。49 形式化驗(yàn)證工具及案例形式化驗(yàn)證工具及案例o時(shí)態(tài)邏輯模型檢驗(yàn)工具有EMC、CESAR、SMV、Mur、SPIN、UV、SVE、HyTech、Kronos等；行為一致檢驗(yàn)工具有FDR、Cospan/Formal Check等；復(fù)合檢驗(yàn)工具有HSIS、VIS、STeP、METAFrame等。o貝爾實(shí)驗(yàn)室對其高級數(shù)據(jù)鏈路控制器在FormalCheck下進(jìn)行了模型檢驗(yàn)功能驗(yàn)證

39、，6個(gè)性能進(jìn)行了規(guī)格，其中5個(gè)驗(yàn)證無誤、另外一個(gè)失敗，從而進(jìn)一步發(fā)現(xiàn)了一個(gè)影響信道流量的Bug；o對某樓宇抗震分布式主動結(jié)構(gòu)控制系統(tǒng)設(shè)計(jì)進(jìn)行了規(guī)格，所生成的系統(tǒng)模型有2.121019數(shù)目的狀態(tài)。經(jīng)過模型檢驗(yàn)分析發(fā)現(xiàn)了影響主動控制效果的計(jì)時(shí)器設(shè)置錯(cuò)誤；o基于SMV輸入語言建立了IEEE Futurebus+896.1-1991標(biāo)準(zhǔn)下cache一致協(xié)議的精確模型，通過SMV驗(yàn)證了模型滿足cache一致性的規(guī)格。并發(fā)現(xiàn)了先前并未找到的潛在協(xié)議設(shè)計(jì)錯(cuò)誤。該工作是第一次從IEEE標(biāo)準(zhǔn)中發(fā)現(xiàn)錯(cuò)誤；oPhilips公司音響設(shè)備的控制協(xié)議通過HyTech得到了完全自動驗(yàn)證，這是一個(gè)具有離散和連續(xù)特征的混雜系統(tǒng)

40、驗(yàn)證問題；oAT&T公司的7500條通信軟件的SDL源代碼進(jìn)行了驗(yàn)證，從中發(fā)現(xiàn)112個(gè)錯(cuò)誤，約55的初始設(shè)計(jì)需求在邏輯上不一致。50 形式化驗(yàn)證工具及應(yīng)用形式化驗(yàn)證工具及應(yīng)用o已有的定理證明器包括：用戶導(dǎo)引自動推演工具有ACL2、Eves、LP、Nqthm、Reve和RRL；證明檢驗(yàn)器有Coq、HOL、LEGO、LCF和Nuprl；復(fù)合證明器Analytica、PVS和Step；o基于符號代數(shù)運(yùn)算的自動定理證明用于證明Pentium中SRT算法的正確性，檢查出了一個(gè)由故障商數(shù)字選擇表引起的錯(cuò)誤；oPowerPC和System/390中寄存器傳輸級、門級、晶體管級的硬件設(shè)計(jì)模擬為布爾狀態(tài)轉(zhuǎn)移函數(shù)

41、，基于OBDD的算法用來檢驗(yàn)不同設(shè)計(jì)級上狀態(tài)轉(zhuǎn)移函數(shù)的等價(jià)性；oNqthm用于Motorola 68020微處理器的規(guī)格，進(jìn)而用來證明不同來源的二進(jìn)制機(jī)器碼的正確性；oACL2用于AMD5K86的浮點(diǎn)除微代碼的規(guī)格和機(jī)械證明，ACL2還用來檢驗(yàn)浮點(diǎn)方根微的正確性，發(fā)現(xiàn)了其中的Bug，并對修改后的微代碼進(jìn)行了正確性機(jī)械證明；oACL2用于Motorola復(fù)數(shù)算術(shù)處理器CSP的完全規(guī)格，同時(shí)對CSP的幾個(gè)算法進(jìn)行了驗(yàn)證；oPVS用于航空電子微處理器AAMP5的規(guī)格和驗(yàn)證，對209條AAMP5指令中的108條進(jìn)行了規(guī)格，驗(yàn)證了11個(gè)有代表性的微代碼。51 程序求精程序求精 o程序求精，又稱為程序變換

42、，是將自動推理和形式化方法相程序求精，又稱為程序變換，是將自動推理和形式化方法相結(jié)合而形成的一門新技術(shù)，它研究從抽象的形式規(guī)格推演出結(jié)合而形成的一門新技術(shù)，它研究從抽象的形式規(guī)格推演出具體的面向計(jì)算機(jī)的程序代碼的全過程具體的面向計(jì)算機(jī)的程序代碼的全過程。o用一個(gè)抽象程度低、過程性強(qiáng)的程序，代替一個(gè)抽象程度高、過程性弱的程序，并保持它們之間功能的一致。o程序的層次：最高層是不能直接執(zhí)行的程序，即規(guī)格規(guī)格，它由抽象的描述語句構(gòu)成；最低層是可以直接執(zhí)行的程序，稱為程序代碼程序代碼，它由可執(zhí)行的命令語句構(gòu)成；o最高層和最低層之間為一系列混合程序，其中既含有抽象的描述語句，又含有可執(zhí)行的命令語句。 52

43、 程序求精程序求精o 程序求精技術(shù)是形式化方法研究的一個(gè)熱點(diǎn)，在已出現(xiàn)的許多相關(guān)技術(shù)中，真正能夠應(yīng)用到實(shí)際軟件開發(fā)過程中的并不多。o 目前比較典型的是IBM Hursly公司以及牛津大學(xué)PRG程序設(shè)計(jì)研究組提出的針對Z規(guī)格的求精方法、以及Carroll Morgan的規(guī)則求精方案。53 形式化方法的形式化方法的發(fā)展歷史發(fā)展歷史 20世紀(jì)50年代后期，Backus提出了巴克斯范式（Backus normal formula，簡稱BNF），作為描述程序設(shè)計(jì)語言語法的元語言；20世紀(jì)60年代，F(xiàn)loyd、Hoare和Manna等開展的程序正確性證明研究推動了形式化方法的發(fā)展，他們試圖用數(shù)學(xué)方法來證明程序的正確性并發(fā)展成為了各種程序驗(yàn)證方法，但是受程序規(guī)模限制這些方法并未達(dá)到預(yù)期的