計算機(jī)科學(xué)與技術(shù)方法論-專題講座

1、計算機(jī)科學(xué)與技術(shù)方法論 專題講座- 軟件開發(fā)的形式化方法 （Formal Methods in Software Development） 參考資料 古天龍，軟件開發(fā)的形式化方法，高等教育出版社，2005 董榮勝，古天龍，計算機(jī)科學(xué)與技術(shù)方法論，人民郵電出 版社，2002 古天龍，蔡國永，網(wǎng)絡(luò)協(xié)議的形式化分析與設(shè)計，電子工 業(yè)出版社，2003 楊文龍，古天龍，軟件工程，電子工業(yè)出版社，2004 Alagar V.S. and Periyasamy K., Specification of Software Systems, Springer-Verlag, New York, 1998 Cla

2、rk E. and Wing J., Formal Methods: State of the Art and Future Direction. CMU-CS-96-178, CMU Computer Science Technical Report, 1996, 1-22 Formal Methods: 專題講座的主要任務(wù)(W2H) W(Why) 為什么要學(xué)習(xí)形式化方法? W(What) 形式化方法的基本原理是什么? H(How) 如何將形式化方法集成到軟件開發(fā)過程? 專題講座-軟件開發(fā)的形式化方法 （一）背景知識（一）背景知識 （二）發(fā)展歷史（二）發(fā)展歷史 （三）（三）相關(guān)內(nèi)容相關(guān)內(nèi)容

3、（四）典型方法（四）典型方法 （一）（一）背景知識背景知識 軟件危機(jī)軟件危機(jī) （1968年年10月北大西洋公約組織月北大西洋公約組織NATO） 開發(fā)成本昂貴開發(fā)成本昂貴 項目進(jìn)度難控項目進(jìn)度難控 質(zhì)量無法保證質(zhì)量無法保證 修改維護(hù)困難修改維護(hù)困難 開發(fā)成本昂貴開發(fā)成本昂貴 1968年，美國花費于軟件的投資高達(dá)60億美元，有些系統(tǒng)，特別是軍用 系統(tǒng)，軟費用要高出硬件費用好幾倍，例如美國全球軍事指揮控制系統(tǒng) 的計算機(jī)硬件費用為1億美元，而軟件費用高達(dá)7.2億美元。 1980年美國政府的財政年度當(dāng)中，計算機(jī)系統(tǒng)方面(軟，硬件與服務(wù))共耗 資達(dá)570億美元，其中320億美元(占總數(shù)的56)用于計算機(jī)軟

4、件方面(與 同年的美國汽車行業(yè)進(jìn)行簡單的比較，美國是當(dāng)時的世界第一汽車生產(chǎn) 大國，汽車的年銷售量為900萬輛，總的銷售額僅為720億美元。 技術(shù)的進(jìn)步使得計算機(jī)硬件的成本持續(xù)降低，而軟件成本則不斷增長， 軟件成本在計算機(jī)系統(tǒng)總成本中所占的比例呈現(xiàn)日益擴(kuò)大的趨勢來自 美國空軍計算機(jī)系統(tǒng)的數(shù)據(jù)表明，1970年，軟件費用約占總費用的60， 1975年達(dá)到72，1980年達(dá)到80，1985年計達(dá)到85。這種增長的速 度是驚人的。（1979年，美國的國防預(yù)算為1258億美元，其中9%用于計 算機(jī)領(lǐng)域，約113億美元。在這113億美元當(dāng)中，91億美元（約占80） 用于軟件投資。僅有22億美元用于硬件設(shè)備）

5、。 項目進(jìn)度難控項目進(jìn)度難控 在研究大型系統(tǒng)時，遇到越來越多的困難。有的系絞干脆失敗了，損失 了大量金錢和人力；有的系統(tǒng)雖然完成了，但性能不理想，或推遲了許 多年，經(jīng)費大大超過預(yù)算。如一個大項目負(fù)責(zé)人所說： “軟件人員太像 皇帝新衣故事中的裁縫了、當(dāng)我來檢查軟件開發(fā)工作時；所得到的回答 好像對我說我們正忙于編織這件帶有魔法的織物。只要等一會兒，你就 會看到這件織物是極其美麗的。但是我什么也看不到，什么也摸不到， 也說不出任何一個有關(guān)的數(shù)字；沒有任何辦法得到一些信息說明事情確 實進(jìn)行的非常順利，而且我已經(jīng)知道許多人最終已經(jīng)編織了一大堆昂貴 的廢物而離去，還有下少人最終什么也沒有作出來。” 為軟件

6、開發(fā)制定進(jìn)度是根困難的事情：通常我們對一個任務(wù)根據(jù)其復(fù)雜性、 工作量及進(jìn)度要求安排人力。如有10人月的工作量，則由一個人完成需 要10個月，由10個入完成則需要一個月。但這種工作量估計方式僅對各 部分工作互下干擾的情況下才適用，例如當(dāng)各部分工作尚能很好地劃分 時，安排由不同人完成不同部分的工作。但作為整體，尚需討論合作， 這種討論交流活動就增加了工作量。軟件系統(tǒng)的結(jié)構(gòu)很復(fù)雜，各部分附 加聯(lián)系極大。增加更多人工作，往往不是縮短時間進(jìn)度，而是會延緩進(jìn) 度。 項目進(jìn)度難控項目進(jìn)度難控（一個例子）（一個例子） 一個軟件項目估計需要12人月工作量。指定由3個人，在4個月內(nèi)完成。假定第1 個月的任務(wù)花了兩

7、個月才完成，如仍需按時完成該怎么辦呢？ （1）假定此任務(wù)只有第一個月的工作量是估計錯了，則到第二個工作月結(jié)束時 ，尚有9個入月工作量必需在兩個月內(nèi)完成，則需用4.5個人。需要增加2個人來 進(jìn)行這項工作； （2）假定此任務(wù)的工作量在每個月都是估計低了。第二月后，尚有18個人月的 工作量要在兩個月內(nèi)完成，則需要9個人工作，即應(yīng)增加6個人。 增加人力的結(jié)果如何呢？在第一種情況下，不論新增加的人的適應(yīng)能力有多強(qiáng)， 總需要有人去幫助他了解熟悉情況。如果這些工作占用了一個月的時間，這樣又 有2個人月工作量是在新的計劃外。同時，為了由5人共同完成工作，又需要花時 間把任務(wù)重新劃分成五個部。這樣，又可能損失一

8、部分已經(jīng)完成的工作，所以到 第三個月結(jié)束時實際上雖有5人在工作，而余留下也許至少是7個入月的工作量， 使任務(wù)仍不能按時完成。如果你仍想按時完成任務(wù)，用投入更多人力的方法可能 造成更壞的后果。 對于一項復(fù)雜的任務(wù)，通常難于通過增加人力來縮短開發(fā)時間。Brook提出的法 則“在已拖延的軟件項目上增加入力只會使其更難按期完成在已拖延的軟件項目上增加入力只會使其更難按期完成” 。這對于一般的 工業(yè)產(chǎn)品來說是難于想象的！ 質(zhì)量無法保證質(zhì)量無法保證 1985年11月21日,由于計算機(jī)軟件的錯誤,造成紐約銀行與美聯(lián)儲電子結(jié)算系統(tǒng)紐約銀行與美聯(lián)儲電子結(jié)算系統(tǒng)收支失衡, 發(fā)生了超額支付,而這個問題一直到晚上才被

9、發(fā)現(xiàn),紐約銀行當(dāng)日帳務(wù)出現(xiàn)了230億的短款。 Therac-25是加拿大原子能公司AECL和一家法國公司CGR聯(lián)合開發(fā)的一種醫(yī)療設(shè)備，它產(chǎn) 生的高能光束或電子流能夠殺死人體毒瘤而不會傷害毒瘤附近的人體健康組織。該設(shè)備 于1982年正式投入生產(chǎn)和使用，在1985年6月到1987年1月的不到兩年的時間里，因為軟 件缺陷引發(fā)了6起由于電子流或X-光束的過量使用的醫(yī)療事故，造成4人死亡、2人重傷 的嚴(yán)重后果。 美國Florida州的福利救濟(jì)系統(tǒng)州的福利救濟(jì)系統(tǒng)用于處理數(shù)百萬受撫養(yǎng)兒童、食品券、醫(yī)療援助等受資助 家庭接受者的資格認(rèn)證，其基于巨型機(jī)系統(tǒng)，支持84個數(shù)據(jù)庫、1390個程序、12000多 個終

10、端和個人計算機(jī)。1992年，該系統(tǒng)的錯誤使得成千上萬的人收到了他們無權(quán)收到的 救濟(jì)，而其他成千上萬急需食品券的人卻排著長隊等待了好幾天。據(jù)后來統(tǒng)計，該錯誤 導(dǎo)致了多支付2.6億美元以及少支付5800萬美元醫(yī)療補(bǔ)助的后果。 1996年，歐洲航天局阿麗亞娜阿麗亞娜5型（型（Ariane5）火箭火箭在發(fā)射后40秒鐘后發(fā)生爆炸，發(fā)射基 地上2名法國士兵當(dāng)場死亡，損耗資產(chǎn)達(dá)10億美元之巨，歷時9年的航天計劃因此嚴(yán)重受 挫。事后專家的調(diào)查分析報告指出，爆炸原因在于慣性導(dǎo)航系統(tǒng)軟件技術(shù)要求和設(shè)計的 錯誤。 2002年，美國商務(wù)部的國立標(biāo)準(zhǔn)技術(shù)研究所（NIST）發(fā)表了一個有關(guān)軟件缺陷的損失的 調(diào)查報告。該報告

11、表示：“據(jù)推測，由于軟件缺陷而引起的損失額每年高達(dá)據(jù)推測，由于軟件缺陷而引起的損失額每年高達(dá)595億美元。億美元。 這一數(shù)字相當(dāng)于美國國內(nèi)生產(chǎn)總值的這一數(shù)字相當(dāng)于美國國內(nèi)生產(chǎn)總值的0.6%”。對于一些安全悠關(guān)的系統(tǒng)，軟件的缺陷更。對于一些安全悠關(guān)的系統(tǒng)，軟件的缺陷更 是造成了災(zāi)難性的后果。是造成了災(zāi)難性的后果。 修改維護(hù)困難修改維護(hù)困難 一個簡單的程序設(shè)計的例子： 某公園有一游船碼頭，負(fù)責(zé)人請一位軟件開發(fā)人員實現(xiàn)計算機(jī)系統(tǒng) 輔助游船管理系統(tǒng)。要求如下：當(dāng)游客向租船處租船時，向租船處查 詢是否有可以租用的船只，如果租船處有空船，管理員就準(zhǔn)備好般只， 幫助游客上船，并在聯(lián)機(jī)終端上打入一信息“S”表

12、示租船周期開始。 計算機(jī)自動把當(dāng)時時鐘值送入信息域。當(dāng)游客還船時，管理員打入另 一信息“E”表示租船周期結(jié)束。由管理員向游客結(jié)算租船時間及費用。 一天結(jié)束時，管理員要用一些管理信息總結(jié)每天工作狀況，要求系統(tǒng) 打印出：租船次數(shù)=NNN，平均租船時間=MMM。顯然，這樣一個系 統(tǒng)的功能包括兩個部分：計算輸入流的信息；打印輸出。 我們知道平均租船時間就是總的時間除以租船次數(shù),總時間的計算為: 總時間 = （第一條租船結(jié)束時間 第一條祖船開始時間） + （第二條 租船結(jié)束時間 第二條祖船開始時間） + = （第一條租船結(jié)束時間 +第二條租船結(jié)束時間+ ） （第一條祖船 開始時間 + 第二條祖船開始時間

13、+ ） 修改維護(hù)困難修改維護(hù)困難 BEGIN Number = 0 Totaltime = 0 Message = 1 WHILE Message GET status IF status = S Totaltime = Totaltime Current-time Number = Number + 1 ELSE Totaltime = Totaltime + Current-time END IF GET Message /”1- start the stream; 0- end of the stream” END WHILE PRINT Number, Totaltime/Number

14、 END 修改維護(hù)困難修改維護(hù)困難 要求找出一天中的最長租用時間。而該軟件開發(fā)人員仔細(xì)檢查這一系統(tǒng)而該軟件開發(fā)人員仔細(xì)檢查這一系統(tǒng) 后，發(fā)現(xiàn)除了把原來程序全部丟掉重新寫一個新程序外，實在無法改寫后，發(fā)現(xiàn)除了把原來程序全部丟掉重新寫一個新程序外，實在無法改寫 原系統(tǒng)，以便包括這一新功能，而重寫新系統(tǒng)的時間或經(jīng)費都是不允許原系統(tǒng)，以便包括這一新功能，而重寫新系統(tǒng)的時間或經(jīng)費都是不允許 的。的。他只好借口某種技術(shù)原因，如機(jī)器操作系統(tǒng)不允許把新要求擴(kuò)充進(jìn) 來。而該負(fù)責(zé)入也不懂得這些技術(shù)名詞，又考慮到這也不算重要向題， 也就同意不再進(jìn)行擴(kuò)充。 要求把每天的報告分成兩個，一個是上午情況，另一個是下午情況。

15、但但 軟件開發(fā)者，仍難于通過修改程序來達(dá)到這一日標(biāo)。軟件開發(fā)者，仍難于通過修改程序來達(dá)到這一日標(biāo)。他只好又推托由于 什么磁盤造成的原因而無法達(dá)到此目標(biāo)。當(dāng)然，負(fù)責(zé)人已經(jīng)不太相信那 些技術(shù)原因，對軟件開發(fā)人員甚為不滿，只好無可奈何地離去。 為了保證游船的安全性，希望知道每艘游船的累計使用時間，以便經(jīng)過 一定的時間運行后進(jìn)行維修保養(yǎng)。然而，負(fù)責(zé)人得到的是開發(fā)人員類似 的答復(fù)。因為除了把原系統(tǒng)廢棄之外，實在無法對其作什么修改來滿足因為除了把原系統(tǒng)廢棄之外，實在無法對其作什么修改來滿足 這一新的重要要求。這一新的重要要求。 這個小故事說明了什么呢？軟件并不像人們想象的那么易于修改！軟件并不像人們想象的

16、那么易于修改！ 修改維護(hù)困難修改維護(hù)困難 軟件的維護(hù)任務(wù)特別重。軟件的維護(hù)任務(wù)特別重。事實上，正式投入使用的商用 軟件，總是存在著一定數(shù)量的錯誤。隨著時間的延伸， 在不同的運行條件下，軟件就會出現(xiàn)故障，就需要維護(hù)。 這種維護(hù)與通常意義下的設(shè)備（硬件）維護(hù)是完全不同 的。因為軟件是邏輯元件，不是一種實物。軟件故障是 軟件中的邏輯故障所造成的，不是硬件的“用舊”、 “磨損”之類問題。軟件維護(hù)不是更換某種備件，而是 要糾正邏輯缺陷。當(dāng)軟件系統(tǒng)變得龐大，問題變得復(fù)雜 時，常常會發(fā)生“糾正一個錯誤帶來更多新的錯誤！” 的問題。 軟件危機(jī)軟件危機(jī) 軟件危機(jī)的原因：軟件危機(jī)的原因： 規(guī)模的復(fù)雜性規(guī)模的復(fù)雜性

17、 結(jié)構(gòu)的復(fù)雜性結(jié)構(gòu)的復(fù)雜性 環(huán)境的復(fù)雜性環(huán)境的復(fù)雜性 領(lǐng)域的復(fù)雜性領(lǐng)域的復(fù)雜性 交流的復(fù)雜性交流的復(fù)雜性 （客觀上）（客觀上） 規(guī)模的復(fù)雜性規(guī)模的復(fù)雜性 隨著計算機(jī)應(yīng)用的日益廣泛，需要開發(fā)的軟件規(guī)模越來 越龐大。以美國宇航局的軟件系統(tǒng)為例：1963年，水星 計劃的軟件系統(tǒng)約有 200萬條指令；1967年，雙子星座 計劃系統(tǒng)約為400萬條指令；1973年，阿波羅計劃系統(tǒng)達(dá) 到1000萬條指令；1979年，哥倫比亞航天飛機(jī)系統(tǒng)更是 達(dá)到了4000萬條指令。軟件龐大的規(guī)模是引起技術(shù)上和 心理上挫折的一個重要因素；此外，規(guī)模的復(fù)雜性引起 了大量學(xué)習(xí)和理解上的負(fù)擔(dān)。由于在需求分析及生成規(guī) 格的階段需要搜

18、集和分析的信息數(shù)量非常巨大，從而可 能會使得信息不正確或不完整，并且在審查階段也未能 檢查出來。正如Leveson 所認(rèn)為的：幾乎所有與計算機(jī)幾乎所有與計算機(jī) 過程控制系統(tǒng)有關(guān)的事故都是源于這類由軟件規(guī)模因素過程控制系統(tǒng)有關(guān)的事故都是源于這類由軟件規(guī)模因素 所引起的錯誤。所引起的錯誤。 結(jié)構(gòu)的復(fù)雜性結(jié)構(gòu)的復(fù)雜性 結(jié)構(gòu)復(fù)雜性體現(xiàn)在管理和技術(shù)兩個方面。在管理方面， 開發(fā)小組用來組織和管理開發(fā)活動時所采用的層次的寬 度和深度，決定了用來管理系統(tǒng)的結(jié)構(gòu)的復(fù)雜性；此外， 軟件開發(fā)機(jī)構(gòu)內(nèi)部的慣例和制度可能會改變各小組之間 的信息流動，從而增加了結(jié)構(gòu)復(fù)雜性。在技術(shù)方面，軟 件系統(tǒng)的模塊結(jié)構(gòu)愈加復(fù)雜，模塊之間

19、復(fù)雜的調(diào)用關(guān)系 以及接口信息往往超過了人們所能接受的程度。這種結(jié) 構(gòu)的復(fù)雜性可以用模塊之間的耦合度來衡量，耦合度反 映了在需求變化的情況下，相應(yīng)所需修改的模塊的數(shù)量。 環(huán)境的復(fù)雜性環(huán)境的復(fù)雜性 首先，運行中的軟件總是受其所處環(huán)境的影響， 在接收到外界環(huán)境的觸發(fā)事件時，軟件應(yīng)該做出 正確的響應(yīng)。為了保證軟件的可靠性，原則上必 須對其所處環(huán)境有很好的理解，對外界環(huán)境可能 產(chǎn)生的所有事件進(jìn)行考慮，但這往往是難以辦到 的。其次，對于許多軟件系統(tǒng)來說，人們往往缺 乏對其所運行的環(huán)境特性的認(rèn)識。許多系統(tǒng)只有 當(dāng)成功地運行于其環(huán)境時，才能對其環(huán)境進(jìn)行很 好的理解。再次，軟件運行環(huán)境的多樣性和異構(gòu) 性給軟件開

20、發(fā)者帶來了更大的挑戰(zhàn)。 領(lǐng)域的復(fù)雜性領(lǐng)域的復(fù)雜性 軟件中所操作的對象僅僅是對應(yīng)用領(lǐng)域真實對象的模擬， 因而軟件開發(fā)者需要從現(xiàn)實世界中抽象出軟件模型所需的 部分，并以其為基礎(chǔ)構(gòu)建軟件。但是對于有的應(yīng)用領(lǐng)域來 說，這些模擬只能是近似的。其原因可能是由于對應(yīng)用領(lǐng) 域?qū)ο蟮恼J(rèn)識不完全，或者是由于該模型所具有的苛刻條 件限制，或者兩者兼而有之。對于一個應(yīng)用工程來說，其 中所使用的模型應(yīng)該是具有合理的科學(xué)理論支持，并且經(jīng) 過良好測試的。然而在某些軟件應(yīng)用領(lǐng)域中，并不存在可 以認(rèn)知的模型，或者沒有準(zhǔn)確的模型來描繪相應(yīng)的物理對 象的幾何、拓?fù)湟约捌渌卣?。在這種缺少準(zhǔn)確認(rèn)識的情 況下，應(yīng)用領(lǐng)域的某些方面很可能

21、在軟件中不能體現(xiàn)出來。 同時，由于有的軟件是根據(jù)近似的模型來構(gòu)建的，因而這 些模型不一定能反映事實情況。 交流的復(fù)雜性交流的復(fù)雜性 由于軟件龐大的規(guī)模、大量的內(nèi)部結(jié)構(gòu)、以及應(yīng)用領(lǐng)域的 不同屬性等因素，在開發(fā)一個大型軟件系統(tǒng)時所參與的不 僅僅是單個的人，而是一個團(tuán)隊。該團(tuán)隊里的每個人參與 開發(fā)過程中的一個或多個活動。此時，對于參與不同開發(fā) 階段的人來說，彼此之間明確的交流非常重要。但是，一 方面，由于結(jié)構(gòu)的復(fù)雜性以及開發(fā)團(tuán)隊的龐大等原因，團(tuán) 隊成員之間的交流非常困難；另一方面，成員之間在進(jìn)行 交流時使用的媒介往往是自然語言、圖、表等非形式化的 方式，這些媒介很難準(zhǔn)確地描述出所開發(fā)的產(chǎn)品的基本屬

22、性，并且，由于這些媒介本身所具有的二義性，往往會使 開發(fā)人員產(chǎn)生錯誤的理解，這種錯誤將會隨著開發(fā)過程的 進(jìn)行而逐漸蔓延開來，最終導(dǎo)致災(zāi)難性的后果。 軟件危機(jī)的原因軟件危機(jī)的原因 缺乏指導(dǎo)或?qū)嵤┸浖O(shè)計、開發(fā)、維護(hù)的缺乏指導(dǎo)或?qū)嵤┸浖O(shè)計、開發(fā)、維護(hù)的 有效理論、方法及技術(shù)有效理論、方法及技術(shù) 或者 缺乏有效解決軟件設(shè)計、開發(fā)、維護(hù)中缺乏有效解決軟件設(shè)計、開發(fā)、維護(hù)中 相關(guān)實際問題的理論、方法及技術(shù)相關(guān)實際問題的理論、方法及技術(shù) （主觀上）（主觀上） 軟件工程軟件工程 19831983年年IEEEIEEE給軟件工程下的定義是：給軟件工程下的定義是：“軟件工程是開發(fā)、遠(yuǎn)行、維護(hù)軟件工程是開發(fā)、遠(yuǎn)行

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

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

25、程化原則。 19931993年年IEEEIEEE進(jìn)一步給出了一個更全面的定義進(jìn)一步給出了一個更全面的定義“軟件上程是：軟件上程是： 把系統(tǒng)把系統(tǒng) 化的、規(guī)范的、可度量的途徑應(yīng)用于軟件并發(fā)、運行和維護(hù)的過程，化的、規(guī)范的、可度量的途徑應(yīng)用于軟件并發(fā)、運行和維護(hù)的過程， 也就是把工程化應(yīng)用于軟件中；也就是把工程化應(yīng)用于軟件中； 研究中提到的途徑。研究中提到的途徑?！?軟件工程軟件工程 工程化的軟件開發(fā)工程化的軟件開發(fā) （類似于建筑、汽車、機(jī)械等其它行業(yè)）（類似于建筑、汽車、機(jī)械等其它行業(yè)） 設(shè)計、生產(chǎn)、維護(hù)的規(guī)范化及科學(xué)化設(shè)計、生產(chǎn)、維護(hù)的規(guī)范化及科學(xué)化 不規(guī)范不規(guī)范規(guī)范；非嚴(yán)格規(guī)范；非嚴(yán)格嚴(yán)格；

26、非形式嚴(yán)格；非形式形式；形式； 無方法無方法/ /技術(shù)技術(shù)方法方法/ /技術(shù)技術(shù) 尋求工程化的軟件開發(fā)的原理、方法及技術(shù)尋求工程化的軟件開發(fā)的原理、方法及技術(shù) 形式化方法形式化方法 形式化方法是滲透在軟件生命期中各個環(huán)節(jié)（如：需求、設(shè)計、實現(xiàn)、形式化方法是滲透在軟件生命期中各個環(huán)節(jié)（如：需求、設(shè)計、實現(xiàn)、 測試等）的數(shù)學(xué)方法測試等）的數(shù)學(xué)方法 或者或者 具有嚴(yán)格數(shù)學(xué)基礎(chǔ)的軟件開發(fā)方法具有嚴(yán)格數(shù)學(xué)基礎(chǔ)的軟件開發(fā)方法 形式化方法的基本含義是借助數(shù)學(xué)的方法來研究計算機(jī)科學(xué)中的有關(guān)形式化方法的基本含義是借助數(shù)學(xué)的方法來研究計算機(jī)科學(xué)中的有關(guān) 問題。問題。 Encyclopedia of Softwar

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

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

29、對軟件的期望特性或 者行為進(jìn)行的精確、簡潔描述。形式化驗證是基于已建立的形式化規(guī)者行為進(jìn)行的精確、簡潔描述。形式化驗證是基于已建立的形式化規(guī) 格，對軟件的相關(guān)特性進(jìn)行評價的數(shù)學(xué)分析和證明。格，對軟件的相關(guān)特性進(jìn)行評價的數(shù)學(xué)分析和證明。 形式化方法形式化方法 形式化方法用于軟件開發(fā)的主要目的是保證軟件的正確性。形式化方法形式化方法用于軟件開發(fā)的主要目的是保證軟件的正確性。形式化方法 基于嚴(yán)格的數(shù)學(xué)，而在軟件開發(fā)過程中使用數(shù)學(xué)具有如下優(yōu)點：數(shù)學(xué)是基于嚴(yán)格的數(shù)學(xué)，而在軟件開發(fā)過程中使用數(shù)學(xué)具有如下優(yōu)點：數(shù)學(xué)是 準(zhǔn)確的建模媒體，能夠?qū)ΜF(xiàn)象、對象、動作等進(jìn)行簡潔、準(zhǔn)確的描述；準(zhǔn)確的建模媒體，能夠?qū)ΜF(xiàn)象、

30、對象、動作等進(jìn)行簡潔、準(zhǔn)確的描述； 數(shù)學(xué)支持抽象，它使得規(guī)格的本質(zhì)可以被展示出來，并且還可以以一種數(shù)學(xué)支持抽象，它使得規(guī)格的本質(zhì)可以被展示出來，并且還可以以一種 有組織的方式來表示系統(tǒng)規(guī)格中的抽象層次；數(shù)學(xué)提供了高層確認(rèn)的手有組織的方式來表示系統(tǒng)規(guī)格中的抽象層次；數(shù)學(xué)提供了高層確認(rèn)的手 段，可以使用數(shù)學(xué)證明來揭示規(guī)格中的矛盾性和不完整性、以及用來展段，可以使用數(shù)學(xué)證明來揭示規(guī)格中的矛盾性和不完整性、以及用來展 示設(shè)計和規(guī)格之間的一致情況等。示設(shè)計和規(guī)格之間的一致情況等。 （從軟件工程知識體角度）2004年年5月，月，IEEE-CS和和ACM聯(lián)合任務(wù)組提交聯(lián)合任務(wù)組提交 了了CCSE（Compu

31、ting Curriculum-Software Engineering）最終報告，在該最終報告，在該 報告給出的報告給出的SEEK（Software Engineering Education Knowledge）中，中，“軟軟 件的形式化方法（件的形式化方法（Formal Methods in Software Engineering）”被單列為一被單列為一 門必修課程（序列號為門必修課程（序列號為SE313）。 （從軟件技術(shù)的最新進(jìn)展）構(gòu)件軟件、軟件體系結(jié)構(gòu)、軟件業(yè)務(wù)工程構(gòu)件軟件、軟件體系結(jié)構(gòu)、軟件業(yè)務(wù)工程 （從軟件開發(fā)方法角度）基于轉(zhuǎn)換模型的軟件開發(fā)（軟件的自動生成）基于轉(zhuǎn)換模型的軟件

32、開發(fā)（軟件的自動生成） 形式化方法形式化方法 需求分析系統(tǒng)設(shè)計I 程序開發(fā) 軟件測試軟件運行 RS codes PS DS-I 系統(tǒng)設(shè)計II 形式化方法形式化方法 基于轉(zhuǎn)換模型的軟件基于轉(zhuǎn)換模型的軟件開發(fā)過程實際上可理解為：從最高層的規(guī)開發(fā)過程實際上可理解為：從最高層的規(guī) 格開始，通過一系列的求精變換步驟，每一步都降低一些抽象格開始，通過一系列的求精變換步驟，每一步都降低一些抽象 程度或增加一些可執(zhí)行性，最終得到能夠指導(dǎo)計算機(jī)明確執(zhí)行程度或增加一些可執(zhí)行性，最終得到能夠指導(dǎo)計算機(jī)明確執(zhí)行 的程序代碼。在進(jìn)行求精的過程中要保證轉(zhuǎn)換之間的一致性和的程序代碼。在進(jìn)行求精的過程中要保證轉(zhuǎn)換之間的一致性

33、和 正確性，保證所得到的程序是滿足最初規(guī)格的。這種正確性和正確性，保證所得到的程序是滿足最初規(guī)格的。這種正確性和 一致性可以通過求精過程中所遵循的一系列規(guī)則來保證，也可一致性可以通過求精過程中所遵循的一系列規(guī)則來保證，也可 以在事后采用驗證工具來證明?；谵D(zhuǎn)換模型的軟件以在事后采用驗證工具來證明?；谵D(zhuǎn)換模型的軟件開發(fā)過程開發(fā)過程 包含了如下三方面的活動：包含了如下三方面的活動： 形式化規(guī)格形式化規(guī)格 形式化驗證形式化驗證 程序求精（程序求精（refinementrefinement）或變換或變換 形式化規(guī)格形式化規(guī)格 軟件規(guī)格是指對軟件系統(tǒng)對象及用來對系統(tǒng)對象進(jìn)行操作的方法集合，以及對所開發(fā)

34、系統(tǒng) 中的各對象在其生存期間里的集體行為的描述。軟件生命周期模型將整個軟件開發(fā)過程分 解為一系列的階段，并為每個階段賦予明確的任務(wù)。雖然在不同的模型中這些階段的分界 和順序有所不同，但規(guī)格在每個階段所產(chǎn)生的作用都使得對系統(tǒng)特征的定義更加準(zhǔn)確。對 系統(tǒng)中的每個對象來說，對象、對象的性質(zhì)以及操作等都應(yīng)該在系統(tǒng)演變的整個過程中當(dāng) 作一個整體來處理。所以，“規(guī)格”應(yīng)當(dāng)理解為一個多階段的、而不是僅僅某一個階段的 行為。 規(guī)格可以采用非形式化的方式來描述，包括自然語言、圖、表等，也可以采用形式化方式 來描述。由于非形式化方法本身所存在的矛盾、二義性、含糊性，以及描述規(guī)格時的不完 整性、抽象層次混雜等情況，

35、使得所得到的規(guī)格不能準(zhǔn)確地刻畫系統(tǒng)模型，甚至?xí)楹髞?的軟件開發(fā)埋下出錯的隱患。而對于形式化方法來說，由于其基于嚴(yán)格的數(shù)學(xué)，具有嚴(yán)格 的語法和語義定義，從而可以準(zhǔn)確地描述系統(tǒng)模型，排除了矛盾、二義性、含糊性等情況； 同時，在對系統(tǒng)進(jìn)行嚴(yán)格地描述的過程中，將會幫助用戶明確其原本模糊的需求，并發(fā)現(xiàn) 用戶所陳述的需求中存在的矛盾等情況，從而相對完整、正確地理解用戶需求，最終得到 一個完整、正確的系統(tǒng)模型。 形式規(guī)格精確地描述了用戶的需求、軟件系統(tǒng)的功能以及各種性質(zhì)，其描述的是“做什 么”，而不考慮“怎么做”。故在書寫規(guī)格時應(yīng)該注意的一個問題是如何描述得恰如其分， 既不過多也不過少。在規(guī)格中描述過多會

36、導(dǎo)致“實現(xiàn)偏向”，給實現(xiàn)施加了不必要的限制， 從而排除了一些原本是合理的實現(xiàn)；描述得過少又有容納不合理實現(xiàn)的危險。為了開發(fā)出 良好的規(guī)格，除了應(yīng)透徹理解、熟練掌握所使用的形式規(guī)格語言和方法外，更重要的是對 所要描述的系統(tǒng)有全面深入的了解。 形式化驗證形式化驗證 形式化驗證的主要技術(shù)包括模型檢驗和定理證明。模型檢驗是一種基于有限 狀態(tài)模型并檢驗該模型的期望特性的技術(shù)。粗略地講，模型檢驗就是對模型 的狀態(tài)空間進(jìn)行蠻力搜索，以確認(rèn)該系統(tǒng)模型是否具有某些性質(zhì)。搜索的可 終止性依賴于模型的有限性。模型檢驗主要適用于有窮狀態(tài)系統(tǒng)，其優(yōu)點是 完全自動化并且驗證速度快；并且，模型檢驗可用于系統(tǒng)部分規(guī)格，即對于

37、 只給出了部分規(guī)格的系統(tǒng)，通過搜索也可以提供關(guān)于已知部分正確性的有用 信息；此外，當(dāng)所檢驗的性質(zhì)未被滿足時，將終止搜索過程并給出反例，這 種信息常常反映了系統(tǒng)設(shè)計中的細(xì)微失誤，因而對于用戶排錯有極大的幫助。 模型檢驗方法的一個嚴(yán)重缺陷是“狀態(tài)爆炸問題”，即隨著所要檢驗的系統(tǒng) 的規(guī)模增大，模型檢驗算法所需的時間/空間開銷往往呈指數(shù)增長，因而極 大限制了其實際使用范圍。 定理證明采用邏輯公式來規(guī)格系統(tǒng)及其性質(zhì)，其中的邏輯由一個具有公理和 推理規(guī)則的形式化系統(tǒng)給出，進(jìn)行定理證明的過程就是應(yīng)用這些公理或推理 規(guī)則來證明系統(tǒng)具有某些性質(zhì)。不同于模型檢驗，定理證明可以處理無限狀 態(tài)空間問題。定理證明系統(tǒng)又

38、可以粗略地分為自動和交互式兩種類型。自動 定理證明系統(tǒng)是通用搜索過程，在解決各種組合問題中比較成功；交互式定 理證明系統(tǒng)需要與用戶進(jìn)行交互，要求用戶能提供驗證中創(chuàng)造性最強(qiáng)部分 （建立斷言等）的工作，因而其效率較低，較難用于大系統(tǒng)的驗證。 程序求精程序求精 程序求精，又稱為程序變換，是將自動推理和形式化方法相結(jié)合 而形成的一門新技術(shù)，它研究從抽象的形式規(guī)格推演出具體的面 向計算機(jī)的程序代碼的全過程。 程序求精的基本思想是用一個抽象程度低、過程性強(qiáng)的程序去代 替一個抽象程度高、過程性弱的程序，并保持它們之間功能的一 致。這里所說的“程序”與傳統(tǒng)觀點中“可以由計算機(jī)直接執(zhí)行” 的“程序”不同，這里的

39、“程序”是對規(guī)格、設(shè)計文檔以及程序 代碼的統(tǒng)稱。在這種理解下，程序可以劃分為若干層次：最高層 是不能直接執(zhí)行的程序，即規(guī)格，它由抽象的描述語句構(gòu)成；最 低層是可以直接執(zhí)行的程序，稱為程序代碼，它由可執(zhí)行的命令 語句構(gòu)成；最高層和最低層之間為一系列混合程序，其中既含有 抽象的描述語句，又含有可執(zhí)行的命令語句。 （二（二）發(fā)展歷史發(fā)展歷史 20世紀(jì)50年代后期，Backus提出了巴克斯范式（Backus normal formula，簡稱BNF），作為描述程序設(shè)計語言語法的元語言； 20世紀(jì)60年代，F(xiàn)loyd、Hoare和Manna等開展的程序正確性證明研究 推動了形式化方法的發(fā)展，他們試圖用數(shù)

40、學(xué)方法來證明程序的正 確性并發(fā)展成為了各種程序驗證方法，但是受程序規(guī)模限制這些 方法并未達(dá)到預(yù)期的應(yīng)用效果； 20世紀(jì)80年代，在硬件設(shè)計領(lǐng)域形式化方法的工業(yè)應(yīng)用結(jié)果，掀起 了軟件形式化開發(fā)方法的學(xué)術(shù)研究和工業(yè)應(yīng)用的熱潮，Pnueli提出 了反應(yīng)式系統(tǒng)規(guī)格和驗證的時態(tài)邏輯(temporal logic，簡稱TL)方法， Clarke和Emerson提出了有窮狀態(tài)并發(fā)系統(tǒng)的模型檢驗(model checking)方法； 20世紀(jì)80年代，牛津大學(xué)和Hursley實驗室于合作將Z用于IBM商用信 息控制系統(tǒng)。IBM對整個開發(fā)所進(jìn)行的測試表明：明顯地改善了 產(chǎn)品質(zhì)量、大量地減少了錯誤和早期診斷錯誤。

41、IBM估計使總體 開發(fā)成本降低9。這一成果獲皇家技術(shù)成就獎； （二（二）發(fā)展歷史發(fā)展歷史 1992年，Praxis公司交付給英國民航局的信息顯示系統(tǒng)是倫敦機(jī)場新空中交通管理系 統(tǒng)的部分。在該系統(tǒng)的需求分析階段，形式化規(guī)格和非形式結(jié)構(gòu)化的需求概念相 結(jié)合。在系統(tǒng)規(guī)格階段，采用了抽象的VDM模型。在設(shè)計階段，抽象VDM細(xì)化為 更為具體的模塊化規(guī)格。項目開發(fā)的生產(chǎn)效率和采用非形式化技術(shù)相當(dāng)、甚至更 好。同時，軟件質(zhì)量得到了很大的提高，軟件的故障率僅為0.75每千行代碼，大 大低于采用非形式化技術(shù)所提供的軟件的故障率（約為220每千行代碼）； 美國加州大學(xué)的安全關(guān)鍵系統(tǒng)研究組所開發(fā)的空中交通防碰撞系統(tǒng)

42、的形式化需求規(guī)格 TCASII，采用了基于Statecharts的需求狀態(tài)機(jī)語言RSML，解決了開發(fā)過程中遇到的 許多問題。TCASII項目表明：復(fù)雜過程控制系統(tǒng)軟件開發(fā)采用形式化需求規(guī)格的可 能性以及應(yīng)用工程師們不經(jīng)任何專門培訓(xùn)建立易讀且易評判的形式化規(guī)格的可行 性。 其它方面的應(yīng)用：數(shù)據(jù)庫：用于存儲病人監(jiān)護(hù)信息的HP醫(yī)用儀器實時數(shù)據(jù)庫系統(tǒng)；電 子儀器：Tektronix系列諧波發(fā)生器、Schlumberger家用電度計；硬件：INMOS浮點 處理器、INMOS中T9000系列的虛擬信道處理器；醫(yī)療設(shè)備：核磁共振理療系統(tǒng)； 核反應(yīng)堆系統(tǒng)：核反應(yīng)器安全系統(tǒng)、核發(fā)電系統(tǒng)的切換裝置；保密系統(tǒng)：NA

43、TO控 制指揮和控制系統(tǒng)中的保密策略模型、Multinet網(wǎng)關(guān)系統(tǒng)的數(shù)據(jù)安全傳輸、美國國 家標(biāo)準(zhǔn)和技術(shù)院的令牌訪問控制系統(tǒng)；電信系統(tǒng)：AT&T的5ESS電話交換系統(tǒng)、德 國電信的電話業(yè)務(wù)系統(tǒng)；運輸系統(tǒng)：巴黎地鐵的自動火車保護(hù)系統(tǒng)、英國鐵路信 號控制、以色列機(jī)載航空電子軟件。 （二（二）發(fā)展歷史發(fā)展歷史 時態(tài)邏輯模型檢驗工具有EMC、CESAR、SMV、Mur、SPIN、UV、SVE、HyTech、 Kronos等；行為一致檢驗工具有FDR、Cospan/Formal Check等；復(fù)合檢驗工 具有HSIS、VIS、STeP、METAFrame等。 貝爾實驗室對其高級數(shù)據(jù)鏈路控制器在Formal

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

45、自動驗證，這是一個具 有離散和連續(xù)特征的混雜系統(tǒng)驗證問題； AT&T公司的7500條通信軟件的SDL源代碼進(jìn)行了驗證，從中發(fā)現(xiàn)112個錯誤，約 55的初始設(shè)計需求在邏輯上不一致。 （二（二）發(fā)展歷史發(fā)展歷史 已有的定理證明器包括：用戶導(dǎo)引自動推演工具有ACL2、Eves、LP、Nqthm、 Reve和RRL；證明檢驗器有Coq、HOL、LEGO、LCF和Nuprl；復(fù)合證明器 Analytica、PVS和Step； 基于符號代數(shù)運算的自動定理證明用于證明Pentium中SRT算法的正確性，檢查 出了一個由故障商數(shù)字選擇表引起的錯誤； PowerPC和System/390中寄存器傳輸級、門級、晶

46、體管級的硬件設(shè)計模擬為布爾 狀態(tài)轉(zhuǎn)移函數(shù)，基于OBDD的算法用來檢驗不同設(shè)計級上狀態(tài)轉(zhuǎn)移函數(shù)的等 價性； Nqthm用于Motorola 68020微處理器的規(guī)格，進(jìn)而用來證明不同來源的二進(jìn)制機(jī) 器碼的正確性； ACL2用于AMD5K86的浮點除微代碼的規(guī)格和機(jī)械證明，ACL2還用來檢驗浮點方 根微的正確性，發(fā)現(xiàn)了其中的Bug，并對修改后的微代碼進(jìn)行了正確性機(jī)械 證明； ACL2用于Motorola復(fù)數(shù)算術(shù)處理器CSP的完全規(guī)格，同時對CSP的幾個算法進(jìn)行了 驗證； PVS用于航空電子微處理器AAMP5的規(guī)格和驗證，對209條AAMP5指令中的108條 進(jìn)行了規(guī)格，驗證了11個有代表性的微代碼

47、。 （二（二）發(fā)展歷史發(fā)展歷史 程序求精技術(shù)是形式化方法研究的一個熱點，在 已出現(xiàn)的許多相關(guān)技術(shù)中，真正能夠應(yīng)用到實際 軟件開發(fā)過程中的并不多。目前比較典型的是 IBM Hursly公司以及牛津大學(xué)PRG程序設(shè)計研究組 提出的針對Z規(guī)格的求精方法、以及Carroll Morgan的規(guī)則求精方案。 （三（三）相關(guān)內(nèi)容相關(guān)內(nèi)容 從形式化規(guī)格到目標(biāo)軟件系統(tǒng)的可實現(xiàn)和可執(zhí)行角度，形式化方法可分為三類： 操作類、描述類和雙重類。 操作類方法基于狀態(tài)和轉(zhuǎn)移，通過可執(zhí)行模型來描述系統(tǒng)，模型本身能夠采用靜 態(tài)分析和模型執(zhí)行而得到驗證，這類方法包括有限狀態(tài)機(jī)、Statecharts、Petri網(wǎng) 等； 描述類方

48、法基于數(shù)學(xué)公理和概念，通過邏輯或代數(shù)給出系統(tǒng)的狀態(tài)空間，具有高 度抽象的特點，便于通過自動工具進(jìn)行驗證?；诓煌臄?shù)學(xué)基礎(chǔ)，描述類方 法進(jìn)一步分為：基于代數(shù)的描述類方法，如Z、VDM、Larch等，和以命題線性時 態(tài)邏輯（propositional linear temporal logic，簡稱PLTL）、一階線性時態(tài)邏輯 （first-order linear temporal logic，簡稱FOLTL）、計算樹邏輯（computation tree temporal logic，簡稱CTL）等時態(tài)邏輯為代表的基于邏輯的描述類方法； 雙重類方法則兼有前面二者的特點，既能夠通過數(shù)學(xué)公理和概

49、念來高度抽象地描述 系統(tǒng)，又具有狀態(tài)和轉(zhuǎn)移的可執(zhí)行特征，這類方法包括擴(kuò)展?fàn)顟B(tài)機(jī)/實時時態(tài)邏 輯（extended state machine / real-time temporal logic，簡稱ESM/RTTL）、TRIO+、 TROL等。 （三（三）相關(guān)內(nèi)容相關(guān)內(nèi)容 形式化方法一直受到多方面的爭議。持肯定態(tài)度的擁護(hù)者認(rèn)為形式化方法會引形式化方法一直受到多方面的爭議。持肯定態(tài)度的擁護(hù)者認(rèn)為形式化方法會引 起軟件開發(fā)的革命，另一些持否定態(tài)度者則懷疑甚至反對將數(shù)學(xué)引入軟件開發(fā)起軟件開發(fā)的革命，另一些持否定態(tài)度者則懷疑甚至反對將數(shù)學(xué)引入軟件開發(fā) 過程中。形式化方法的一些爭議或缺陷主要體現(xiàn)在：形

50、式化方法中所包含的數(shù)過程中。形式化方法的一些爭議或缺陷主要體現(xiàn)在：形式化方法中所包含的數(shù) 學(xué)理論，限制了大多數(shù)程序設(shè)計人員的學(xué)習(xí)和使用；采用形式化開發(fā)方法會延學(xué)理論，限制了大多數(shù)程序設(shè)計人員的學(xué)習(xí)和使用；采用形式化開發(fā)方法會延 誤項目開發(fā)周期、增加開發(fā)費用；許多流行的形式化方法對于較小規(guī)模項目是誤項目開發(fā)周期、增加開發(fā)費用；許多流行的形式化方法對于較小規(guī)模項目是 有效的，但卻很難應(yīng)用于一些大型系統(tǒng)；形式化方法不能確保開發(fā)出完全正確有效的，但卻很難應(yīng)用于一些大型系統(tǒng)；形式化方法不能確保開發(fā)出完全正確 的軟件；缺乏對軟件生命周期內(nèi)各個階段提供全面支持的形式化方法等。的軟件；缺乏對軟件生命周期內(nèi)各個階段提供全面支持的形式化方法等。 形式化方法中的抽象數(shù)學(xué)符號及理論確實對軟件工程師的使用帶來一些不便，形式化方法中的抽象數(shù)學(xué)符號及理論確實對軟件工程師的使用帶來一些不便， 以致于人們要花