軟件開發(fā)的形式化方法和規(guī)格

1、軟件開發(fā)的形式化方法和規(guī)格 第1章 軟件及其開發(fā)概述-3-內(nèi)容安排軟件開發(fā)的歷史軟件危機軟件工程形式化開發(fā)方法-4-1.1 軟件開發(fā)的歷史軟件軟件開發(fā)把現(xiàn)實世界的需求反映成軟件的模型化并予以實現(xiàn)的過程軟件及開發(fā)的三個階段程序設(shè)計階段（1946年-1956年）科學計算、機器語言及匯編語言、個體編程編程技巧、程序效率沒有文檔、軟件一詞尚未出現(xiàn)-5-1.1 軟件開發(fā)的歷史軟件及開發(fā)的三個階段程序系統(tǒng)階段（1956年-1968年）1956年，J.Backus(77) Fortran語言誕生大量數(shù)據(jù)處理、小組開發(fā)“軟件”一詞出現(xiàn)：程序及其說明60年代中期，軟件危機。軟件工程階段（1968年以來）1968

2、年NATO會議，提出“軟件工程”術(shù)語工程化方法、描述語言、團隊開發(fā)軟件的定義 當它被執(zhí)行時能夠提供所要求的功能和性能的指令或計算機程序 使得該程序能夠滿意地處理信息的數(shù)據(jù)結(jié)構(gòu) 描述程序的功能需求以及程序的操作和使用文檔-6-1.2 軟件危機1968年，NATO會議提出了“軟件危機”一詞軟件危機包含兩方面問題如何開發(fā)軟件，以滿足不斷增長、日趨復(fù)雜的需求；如何維護數(shù)量不斷膨脹的軟件產(chǎn)品。軟件危機主要表現(xiàn)如下幾個方面開發(fā)成本昂貴項目進度難控質(zhì)量無法保證修改維護困難 -7-開發(fā)成本昂貴1968年，美國花費于軟件的投資高達60億美元，有些系統(tǒng)，特別是軍用系統(tǒng)，軟費用要高出硬件費用好幾倍，例如美國全球軍事

3、指揮控制系統(tǒng)的計算機硬件費用為1億美元，而軟件費用高達7.2億美元。1980年美國政府的財政年度當中，計算機系統(tǒng)方面(軟，硬件與服務(wù))共耗資達570億美元，其中320億美元(占總數(shù)的56)用于計算機軟件方面(與同年的美國汽車行業(yè)進行簡單的比較，美國是當時的世界第一汽車生產(chǎn)大國，汽車的年銷售量為900萬輛，總的銷售額僅為720億美元。技術(shù)的進步使得計算機硬件的成本持續(xù)降低，而軟件成本則不斷增長，軟件成本在計算機系統(tǒng)總成本中所占的比例呈現(xiàn)日益擴大的趨勢來自美國空軍計算機系統(tǒng)的數(shù)據(jù)表明，1970年，軟件費用約占總費用的60，1975年達到72，1980年達到80，1985年計達到85。這種增長的速度

4、是驚人的。（1979年，美國的國防預(yù)算為1258億美元，其中9%用于計算機領(lǐng)域，約113億美元。在這113億美元當中，91億美元（約占80）用于軟件投資。僅有22億美元用于硬件設(shè)備）。-8-項目進度難控在研究大型系統(tǒng)時，遇到越來越多的困難。有的系絞干脆失敗了，損失了大量金錢和人力；有的系統(tǒng)雖然完成了，但性能不理想，或推遲了許多年，經(jīng)費大大超過預(yù)算。如一個大項目負責人所說： “軟件人員太像皇帝新衣故事中的裁縫了、當我來檢查軟件開發(fā)工作時；所得到的回答好像對我說我們正忙于編織這件帶有魔法的織物。只要等一會兒，你就會看到這件織物是極其美麗的。但是我什么也看不到，什么也摸不到，也說不出任何一個有關(guān)的數(shù)

5、字；沒有任何辦法得到一些信息說明事情確實進行的非常順利，而且我已經(jīng)知道許多人最終已經(jīng)編織了一大堆昂貴的廢物而離去，還有下少人最終什么也沒有作出來。”為軟件開發(fā)制定進度是根困難的事情：通常我們對一個任務(wù)根據(jù)其復(fù)雜性、工作量及進度要求安排人力。如有10人月的工作量，則由一個人完成需要10個月，由10個入完成則需要一個月。但這種工作量估計方式僅對各部分工作互下干擾的情況下才適用，例如當各部分工作尚能很好地劃分時，安排由不同人完成不同部分的工作。但作為整體，尚需討論合作，這種討論交流活動就增加了工作量。軟件系統(tǒng)的結(jié)構(gòu)很復(fù)雜，各部分附加聯(lián)系極大。增加更多人工作，往往不是縮短時間進度，而是會延緩進度。 -

6、9-項目進度難控對于一項復(fù)雜的任務(wù)，通常難于通過增加人力來縮短開發(fā)時間。Brook提出的法則“在已拖延的軟件項目上增加入力只會使其更難按期完成” 。這對于一般的工業(yè)產(chǎn)品來說是難于想象的！1995年，美國共取消810億美元的軟件項目，其中31%未完取消，53%的項目延長一半時間，9%按期完成且不超期。1998年，美國企業(yè)應(yīng)用項目不成功比率75%,其中28%的項目取消，40%無限拖長且資金超出預(yù)賽對于一項復(fù)雜的任務(wù)，通常難于通過增加人力來縮短開發(fā)時間。Brook提出的法則“在已拖延的軟件項目上增加入力只會使其更難按期完成” 。這對于一般的工業(yè)產(chǎn)品來說是難于想象的！-10-質(zhì)量無法保證1985年11

7、月21日,由于計算機軟件的錯誤,造成紐約銀行與美聯(lián)儲電子結(jié)算系統(tǒng)收支失衡,發(fā)生了超額支付,而這個問題一直到晚上才被發(fā)現(xiàn),紐約銀行當日帳務(wù)出現(xiàn)了230億的短款。Therac-25是加拿大原子能公司AECL和一家法國公司CGR聯(lián)合開發(fā)的一種醫(yī)療設(shè)備，它產(chǎn)生的高能光束或電子流能夠殺死人體毒瘤而不會傷害毒瘤附近的人體健康組織。在1985年6月到1987年1月，因為軟件缺陷引發(fā)了6起由于電子流或X-光束的過量使用的醫(yī)療事故，造成4人死亡、2人重傷的嚴重后果。美國Florida州的福利救濟系統(tǒng)用于處理數(shù)百萬受撫養(yǎng)兒童、食品券、醫(yī)療援助等受資助家庭接受者的資格認證，其基于巨型機系統(tǒng)，支持84個數(shù)據(jù)庫、139

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

9、的0.6%”-11-軟件維護困難軟件的維護任務(wù)特別重。事實上，正式投入使用的商用軟件，總是存在著一定數(shù)量的錯誤。隨著時間的延伸，在不同的運行條件下，軟件就會出現(xiàn)故障，就需要維護。這種維護與通常意義下的設(shè)備（硬件）維護是完全不同的。因為軟件是邏輯元件，不是一種實物。軟件故障是軟件中的邏輯故障所造成的，不是硬件的“用舊”、“磨損”之類問題。軟件維護不是更換某種備件，而是要糾正邏輯缺陷。當軟件系統(tǒng)變得龐大，問題變得復(fù)雜時，常常會發(fā)生“糾正一個錯誤帶來更多新的錯誤！”的問題。 新的錯誤發(fā)現(xiàn)、運行環(huán)境的改變、用戶提出新要求，軟件需不斷修改沒有遵循標準、沒有準確的文檔，維護困難巨大。-12-軟件危機的原因

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

11、，并且在審查階段也未能檢查出來。正如Leveson 所認為的：幾乎所有與計算機過程控制系統(tǒng)有關(guān)的事故都是源于這類由軟件規(guī)模因素所引起的錯誤。-14-結(jié)構(gòu)的復(fù)雜性結(jié)構(gòu)復(fù)雜性體現(xiàn)在管理和技術(shù)兩個方面。在管理方面，開發(fā)小組用來組織和管理開發(fā)活動時所采用的層次的寬度和深度，決定了用來管理系統(tǒng)的結(jié)構(gòu)的復(fù)雜性；此外，軟件開發(fā)機構(gòu)內(nèi)部的慣例和制度可能會改變各小組之間的信息流動，從而增加了結(jié)構(gòu)復(fù)雜性。在技術(shù)方面，軟件系統(tǒng)的模塊結(jié)構(gòu)愈加復(fù)雜，模塊之間復(fù)雜的調(diào)用關(guān)系以及接口信息往往超過了人們所能接受的程度。這種結(jié)構(gòu)的復(fù)雜性可以用模塊之間的耦合度來衡量，耦合度反映了在需求變化的情況下，相應(yīng)所需修改的模塊的數(shù)量。-1

12、5-環(huán)境的復(fù)雜性首先，運行中的軟件總是受其所處環(huán)境的影響，在接收到外界環(huán)境的觸發(fā)事件時，軟件應(yīng)該做出正確的響應(yīng)。為了保證軟件的可靠性，原則上必須對其所處環(huán)境有很好的理解，對外界環(huán)境可能產(chǎn)生的所有事件進行考慮，但這往往是難以辦到的。其次，對于許多軟件系統(tǒng)來說，人們往往缺乏對其所運行的環(huán)境特性的認識。許多系統(tǒng)只有當成功地運行于其環(huán)境時，才能對其環(huán)境進行很好的理解。再次，軟件運行環(huán)境的多樣性和異構(gòu)性給軟件開發(fā)者帶來了更大的挑戰(zhàn)。-16-領(lǐng)域的復(fù)雜性 軟件中所操作的對象僅僅是對應(yīng)用領(lǐng)域真實對象的模擬，因而軟件開發(fā)者需要從現(xiàn)實世界中抽象出軟件模型所需的部分，并以其為基礎(chǔ)構(gòu)建軟件。但是對于有的應(yīng)用領(lǐng)域來說

13、，這些模擬只能是近似的。其原因可能是由于對應(yīng)用領(lǐng)域?qū)ο蟮恼J識不完全，或者是由于該模型所具有的苛刻條件限制，或者兩者兼而有之。對于一個應(yīng)用工程來說，其中所使用的模型應(yīng)該是具有合理的科學理論支持，并且經(jīng)過良好測試的。然而在某些軟件應(yīng)用領(lǐng)域中，并不存在可以認知的模型，或者沒有準確的模型來描繪相應(yīng)的物理對象的幾何、拓撲以及其它特征。在這種缺少準確認識的情況下，應(yīng)用領(lǐng)域的某些方面很可能在軟件中不能體現(xiàn)出來。同時，由于有的軟件是根據(jù)近似的模型來構(gòu)建的，因而這些模型不一定能反映事實情況。-17-交流的復(fù)雜性由于軟件龐大的規(guī)模、大量的內(nèi)部結(jié)構(gòu)、以及應(yīng)用領(lǐng)域的不同屬性等因素，在開發(fā)一個大型軟件系統(tǒng)時所參與的不僅

14、僅是單個的人，而是一個團隊。該團隊里的每個人參與開發(fā)過程中的一個或多個活動。此時，對于參與不同開發(fā)階段的人來說，彼此之間明確的交流非常重要。一方面，由于結(jié)構(gòu)的復(fù)雜性以及開發(fā)團隊的龐大等原因，團隊成員之間的交流非常困難；另一方面，成員之間在進行交流時使用的媒介往往是自然語言、圖、表等非形式化的方式，這些媒介很難準確地描述出所開發(fā)的產(chǎn)品的基本屬性，并且，由于這些媒介本身所具有的二義性，往往會使開發(fā)人員產(chǎn)生錯誤的理解，這種錯誤將會隨著開發(fā)過程的進行而逐漸蔓延開來，最終導(dǎo)致災(zāi)難性的后果。 -18-軟件危機？軟件危機的原因缺乏指導(dǎo)或?qū)嵤┸浖O(shè)計、開發(fā)、維護的有效理論、方法及技術(shù) 或者缺乏有效解決軟件設(shè)計

15、、開發(fā)、維護中相關(guān)實際問題的理論、方法及技術(shù) 解決方案軟件工程：工程的方法組織和管理形式化方法：正確性和可靠性-19-1.3 軟件工程NATO、軟件工程的定義1983年IEEE給軟件工程下的定義是：“軟件工程是開發(fā)、遠行、維護和修復(fù)軟件的系統(tǒng)方法”。主要強調(diào)軟件工程是系統(tǒng)方法而不是某種神秘的個人技巧。 Fairly認為：“軟件工程學是為了在成本限額以內(nèi)按時完成開發(fā)和修改軟件產(chǎn)品所需要的系統(tǒng)生產(chǎn)和維護技術(shù)及管理學科?！?軟件工程的目標：成本限額、按時完成，軟件工程包含技術(shù)和管理。 Fritz Bauer給出了下述定義：“軟件工程是為了經(jīng)濟地獲得可靠的且能在實際機器上有效運行的軟件，而建立和使用的

16、完善的工程化原則?！辈粌H指出軟件工程的目標是經(jīng)濟地開發(fā)出高質(zhì)量的軟什，而且強調(diào)了軟件工程是一門工程學科，應(yīng)建立并使用完善的工程化原則。1993年IEEE進一步給出了一個更全面的定義“軟件工程是： 把系統(tǒng)化的、規(guī)范的、可度量的途徑應(yīng)用于軟件并發(fā)、運行和維護的過程，也就是把工程化應(yīng)用于軟件中； 研究中提到的途徑。”-20-軟件工程目標、內(nèi)容目標成功地生產(chǎn)具有正確性、可用性以及開銷合宜的產(chǎn)品。三要素方法：構(gòu)造軟件的技術(shù)工具：自動化、半自動化的支持過程：綜合運用方法和工具分步內(nèi)容軟件工程過程、生命周期、開發(fā)模型、開發(fā)方法、工具開發(fā)環(huán)境、計算機輔助軟件工程、軟件工程經(jīng)濟學-21-軟件工程過程規(guī)定了獲取、

17、供應(yīng)、開發(fā)、操作以及維護軟件時，所需要實施的過程、活動和任務(wù)。包括：開發(fā)過程：分析、設(shè)計、編碼、集成、測試、安裝和驗收管理過程：范圍定義、計劃、實施和控制、評審評價、完成供應(yīng)過程：供方按合同提供系統(tǒng)、軟件、服務(wù)獲取過程：需方操作過程：運行系統(tǒng)維護過程：修改支持過程：生命周期的支持-22-軟件生命周期五個活動需求分析和規(guī)格軟件設(shè)計：邏輯模型轉(zhuǎn)換為軟件方案，總體結(jié)構(gòu)、模塊算法代碼編寫軟件測試：模塊測試、組裝測試、確認測試運行維護-23-軟件開發(fā)模型組織軟件生命周期內(nèi)的各種活動：次序、任務(wù)、準則瀑布模型（Winston Royce 1970)計劃任務(wù)書、需求規(guī)格、設(shè)計規(guī)格、程序、測試、維護缺點：需求

18、分析的準確性問題、錯誤反饋不及時、進度難以控制原型模型快速成型、評估、反饋、改進缺點：用戶不理解、開發(fā)人員的惰性不愿意優(yōu)化-24-軟件開發(fā)模型螺旋模型 （Barry W.Boehm,1988）制定計劃、風險評估、實施工程、用戶評價-演化缺點：豐富的評估經(jīng)驗和專業(yè)知識，要求高構(gòu)件模型 即插即用編程標識、選用、組裝，構(gòu)件庫優(yōu)點：生產(chǎn)率、可靠、靈活、可維護-25-軟件開發(fā)模型四代技術(shù)模型（4GT)基于一系列軟件工具的開發(fā)核心：規(guī)格軟件的能力不支持軟件開發(fā)的全過程側(cè)重：設(shè)計階段、實現(xiàn)階段、支持界面缺點：維護問題變換模型基于形式化規(guī)格及程序變換的開發(fā)模型，自動程序設(shè)計模型或形式化方法模型三個核心活動：規(guī)

19、格生成、形式化驗證、計算機輔助程序求精高效、可靠、可控，但要求高-26-軟件開發(fā)方法軟件開發(fā)方法是指在某種思想的指導(dǎo)下使用已經(jīng)定義好的一系列技術(shù)和表示工具來組織軟件開發(fā)過程的方法一般表述成一系列步驟典型的傳統(tǒng)軟件開發(fā)方法：結(jié)構(gòu)化方法面向數(shù)據(jù)結(jié)構(gòu)方法面向?qū)ο蟮拈_發(fā)方法-27-軟件工具輔助軟件開發(fā)、維護和管理的一系列軟件種類繁多管理工具、配置工具、分析設(shè)計工具、編碼工具、測試工具測試工具：數(shù)據(jù)獲取、靜態(tài)分析、動態(tài)測試、模擬、測試管理維護工具：版本控制、文檔分析、開發(fā)信息庫、逆向過程等-28-軟件開發(fā)環(huán)境支持軟件產(chǎn)品生產(chǎn)的軟件系統(tǒng)，由軟件工具和集成機制組成。軟件工具集成機制：為工具集成和軟件的開發(fā)、

20、管理，以及維護提供統(tǒng)一的支持。前端開發(fā)環(huán)境、后端開發(fā)環(huán)境、軟件維護環(huán)境、逆向工程環(huán)境-29-計算機輔助軟件工程實現(xiàn)軟件生命周期各個環(huán)節(jié)的自動化整個生命周期的支持，解決生產(chǎn)效率軟件工程經(jīng)濟學從經(jīng)濟學的觀點來研究、分析如何有效地開發(fā)、發(fā)布軟件產(chǎn)品和支持用戶使用成本估算技術(shù)、模型、效益分析、多目標決策、不確定性的處理、風險分析、工期估計-30-1.4 形式化方法形式化方法概念發(fā)展目的形式化方法軟件開發(fā) 變換模型形式化規(guī)格形式化驗證程序求精形式化方法的應(yīng)用-31-形式化方法概念形式化方法是滲透在軟件生命期中各個環(huán)節(jié)（如：需求、設(shè)計、實現(xiàn)、測試等）的數(shù)學方法 或者 具有嚴格數(shù)學基礎(chǔ)的軟件開發(fā)方法形式化方

21、法的基本含義是借助數(shù)學的方法來研究計算機科學中的有關(guān)問題。Encyclopedia of Software Engineering對形式化方法定義為：“用于開發(fā)計算機系統(tǒng)的形式化方法是基于數(shù)學的用于描述系統(tǒng)性質(zhì)的技術(shù)。這樣的形式化方法提供了一個框架，人們可以在該框架中以系統(tǒng)的方式刻畫、開發(fā)和驗證系統(tǒng)”。 -32-形式化方法概念在軟件開發(fā)的全過程中，凡是采用嚴格的數(shù)學語言，具有精確的數(shù)學語義的方法，都稱為形式化方法。從廣義角度，形式化方法是軟件開發(fā)過程中分析、設(shè)計及實現(xiàn)的系統(tǒng)工程方法。狹義地，形式化方法是軟件規(guī)格（specification）和驗證（verification）的方法。形式化方法又

22、分為形式化規(guī)格方法和形式化驗證方法。形式化規(guī)格是通過具有明確數(shù)學定義的文法和語義的方法或語言對軟件的期望特性或者行為進行的精確、簡潔描述。形式化驗證是基于已建立的形式化規(guī)格，對軟件的相關(guān)特性進行評價的數(shù)學分析和證明。-33-發(fā)展歷史20世紀50年代后期，Backus（77）提出了巴克斯范式（Backus normal formula，簡稱BNF），作為描述程序設(shè)計語言語法的元語言；20世紀60年代，F(xiàn)loyd（78）、Hoare（80）和Manna等開展的程序正確性證明研究推動了形式化方法的發(fā)展，他們試圖用數(shù)學方法來證明程序的正確性并發(fā)展成為了各種程序驗證方法，但是受程序規(guī)模限制這些方法并未達

23、到預(yù)期的應(yīng)用效果；20世紀80年代，在硬件設(shè)計領(lǐng)域形式化方法的工業(yè)應(yīng)用結(jié)果，掀起了軟件形式化開發(fā)方法的學術(shù)研究和工業(yè)應(yīng)用的熱潮，Pnueli(96)提出了反應(yīng)式系統(tǒng)規(guī)格和驗證的時態(tài)邏輯(temporal logic，簡稱TL)方法，Clarke、Emerson、Sifakis(07)提出了有窮狀態(tài)并發(fā)系統(tǒng)的模型檢驗(model checking)方法；近十年來，建立了易于理解的規(guī)格概念和術(shù)語、形式化規(guī)格方法及語言、形式化驗證技術(shù):模型檢測和定理證明，開發(fā)了支撐工具和環(huán)境-35-形式化方法主要目標形式化方法用于軟件開發(fā)的主要目的是保證軟件的正確性。形式化方法基于嚴格的數(shù)學，而在軟件開發(fā)過程中使用

24、數(shù)學具有如下優(yōu)點：數(shù)學是準確的建模媒體，能夠?qū)ΜF(xiàn)象、對象、動作等進行簡潔、準確的描述；數(shù)學支持抽象，它使得規(guī)格的本質(zhì)可以被展示出來，并且還可以以一種有組織的方式來表示系統(tǒng)規(guī)格中的抽象層次；數(shù)學提供了高層確認的手段，可以使用數(shù)學證明來揭示規(guī)格中的矛盾性和不完整性、以及用來展示設(shè)計和規(guī)格之間的一致情況等。 （從軟件工程知識體角度）2004年5月，IEEE-CS和ACM聯(lián)合任務(wù)組提交了CCSE（Computing Curriculum-Software Engineering）最終報告，在該報告給出的SEEK（Software Engineering Education Knowledge）中，“軟

25、件的形式化方法（Formal Methods in Software Engineering）”被單列為一門必修課程（序列號為SE313）。-36-形式化方法軟件開發(fā)變化模型：把現(xiàn)實世界的需求反映成軟件的模型化過程模型化涉及：現(xiàn)實世界、模型表示、計算機系統(tǒng)開發(fā)過程的任務(wù)分為：模型獲取、模型驗證、模型變換模型獲取：從現(xiàn)實世界向模型表示轉(zhuǎn)換，對應(yīng)軟件生命周期中的需求分析、規(guī)格、設(shè)計活動模型驗證：是否滿足需求及具有所期望的特性模型變換：從模型表示向計算機系統(tǒng)變換的過程。關(guān)鍵任務(wù)是一致性測試，對應(yīng)軟件生命周期中的實現(xiàn)和測試這些任務(wù)對應(yīng)三方面的活動：形式化規(guī)格、形式化驗證、程序求精-37-（1）形式化規(guī)

26、格軟件規(guī)格是指對軟件系統(tǒng)對象及用來對系統(tǒng)對象進行操作的方法集合，以及對所開發(fā)系統(tǒng)中的各對象在其生存期間里的集體行為的描述。軟件生命周期模型將整個軟件開發(fā)過程分解為一系列的階段，并為每個階段賦予明確的任務(wù)。 “規(guī)格”應(yīng)當理解為一個多階段的、而不是僅僅某一個階段的行為。 需求分析系統(tǒng)設(shè)計I程序開發(fā)軟件測試軟件運行BS codesPSDS系統(tǒng)設(shè)計II-38-（1）形式化規(guī)格規(guī)格可以采用非形式化的方式來描述，包括自然語言、圖、表等，也可以采用形式化方式來描述。由于非形式化方法本身所存在的矛盾、二義性、含糊性，以及描述規(guī)格時的不完整性、抽象層次混雜等情況，使得所得到的規(guī)格不能準確地刻畫系統(tǒng)模型，甚至會為

27、后來的軟件開發(fā)埋下出錯的隱患。而對于形式化方法來說，由于其基于嚴格的數(shù)學，具有嚴格的語法和語義定義，從而可以準確地描述系統(tǒng)模型，排除了矛盾、二義性、含糊性等情況；同時，在對系統(tǒng)進行嚴格地描述的過程中，將會幫助用戶明確其原本模糊的需求，并發(fā)現(xiàn)用戶所陳述的需求中存在的矛盾等情況，從而相對完整、正確地理解用戶需求，最終得到一個完整、正確的系統(tǒng)模型。-39-（1）形式化規(guī)格形式規(guī)格精確地描述了用戶的需求、軟件系統(tǒng)的功能以及各種性質(zhì)，其描述的是“做什么”，而不考慮“怎么做”。故在書寫規(guī)格時應(yīng)該注意的一個問題是如何描述得恰如其分，既不過多也不過少。在規(guī)格中描述過多會導(dǎo)致“實現(xiàn)偏向”，給實現(xiàn)施加了不必要的限

28、制，從而排除了一些原本是合理的實現(xiàn)；描述得過少又有容納不合理實現(xiàn)的危險。為了開發(fā)出良好的規(guī)格，除了應(yīng)透徹理解、熟練掌握所使用的形式規(guī)格語言和方法外，更重要的是對所要描述的系統(tǒng)有全面深入的了解。-40-（1）形式化規(guī)格形式化規(guī)約的分類:操作類方法：基于狀態(tài)和轉(zhuǎn)移，通過可執(zhí)行模型來描述系統(tǒng)，模型本身能夠采用靜態(tài)分析和模型執(zhí)行而得到驗證，這類方法包括有限狀態(tài)機、Statecharts、Petri網(wǎng)等描述類方法：基于數(shù)學公理和概念，通過邏輯或代數(shù)給出系統(tǒng)的狀態(tài)空間，是高度抽象的，便于通過自動工具進行驗證。包括基于代數(shù)的Z、VDM、Larch等方法，和基于時態(tài)邏輯的PLTL、FOLTL、CTTL方法雙重

29、類方法：兼有前面二者的特點，既能夠通過數(shù)學公理和概念來高度抽象地描述系統(tǒng)，又具有狀態(tài)和轉(zhuǎn)移的可執(zhí)行特征，這類方法包括擴展狀態(tài)機/實時時態(tài)邏輯(ESM/RTTL)、TRIO+、TROL等-41-（1）形式化規(guī)格形式化規(guī)格實例20世紀80年代，牛津大學和Hursley實驗室于合作將Z用于IBM商用信息控制系統(tǒng)。IBM對整個開發(fā)所進行的測試表明：明顯地改善了產(chǎn)品質(zhì)量、大量地減少了錯誤和早期診斷錯誤。IBM估計使總體開發(fā)成本降低9。這一成果獲皇家技術(shù)成就獎；1992年，Praxis公司交付給英國民航局的信息顯示系統(tǒng)是倫敦機場新空中交通管理系統(tǒng)的部分。在系統(tǒng)規(guī)格階段，采用了抽象的VDM模型。在設(shè)計階段，

30、抽象VDM細化為更為具體的模塊化規(guī)格。項目開發(fā)的生產(chǎn)效率和采用非形式化技術(shù)相當、甚至更好。同時，軟件質(zhì)量得到了很大的提高，軟件的故障率僅為0.75每千行代碼，大大低于采用非形式化技術(shù)所提供的軟件的故障率（約為220每千行代碼）；美國加州大學的安全關(guān)鍵系統(tǒng)研究組所開發(fā)的空中交通防碰撞系統(tǒng)的形式化需求規(guī)格TCASII，采用了基于Statecharts的需求狀態(tài)機語言RSML，解決了開發(fā)過程中遇到的許多問題。-42-（1）形式化規(guī)格形式化規(guī)格實例其它方面的應(yīng)用：數(shù)據(jù)庫：用于存儲病人監(jiān)護信息的HP醫(yī)用儀器實時數(shù)據(jù)庫系統(tǒng)；電子儀器：Tektronix系列諧波發(fā)生器、Schlumberger家用電度計；硬

31、件：INMOS浮點處理器、INMOS中T9000系列的虛擬信道處理器；醫(yī)療設(shè)備：核磁共振理療系統(tǒng)；核反應(yīng)堆系統(tǒng)：核反應(yīng)器安全系統(tǒng)、核發(fā)電系統(tǒng)的切換裝置；保密系統(tǒng)：NATO控制指揮和控制系統(tǒng)中的保密策略模型、Multinet網(wǎng)關(guān)系統(tǒng)的數(shù)據(jù)安全傳輸、美國國家標準和技術(shù)院的令牌訪問控制系統(tǒng)；電信系統(tǒng)：AT&T的5ESS電話交換系統(tǒng)、德國電信的電話業(yè)務(wù)系統(tǒng)；運輸系統(tǒng)：巴黎地鐵的自動火車保護系統(tǒng)、英國鐵路信號控制、以色列機載航空電子軟件。-43-（2）形式化驗證主要技術(shù)：模型檢測和定理證明模型檢測模型檢驗是一種基于有限狀態(tài)模型并檢驗該模型的期望特性的技術(shù)。粗略地講，模型檢驗就是對模型的狀態(tài)空間進行蠻力搜

32、索，以確認該系統(tǒng)模型是否具有某些性質(zhì)。搜索的可終止性依賴于模型的有限性。模型檢驗主要適用于有窮狀態(tài)系統(tǒng)，其優(yōu)點是完全自動化并且驗證速度快；并且，模型檢驗可用于系統(tǒng)部分規(guī)格，即對于只給出了部分規(guī)格的系統(tǒng)，通過搜索也可以提供關(guān)于已知部分正確性的有用信息；此外，當所檢驗的性質(zhì)未被滿足時，將終止搜索過程并給出反例，這種信息常常反映了系統(tǒng)設(shè)計中的細微失誤，因而對于用戶排錯有極大的幫助。模型檢驗方法的一個嚴重缺陷是“狀態(tài)爆炸問題”，即隨著所要檢驗的系統(tǒng)的規(guī)模增大，模型檢驗算法所需的時間/空間開銷往往呈指數(shù)增長，因而極大限制了其實際使用范圍。 10120-44-（2）形式化驗證模型檢測工具時態(tài)邏輯模型檢驗工

33、具有EMC、CESAR、SMV、Mur、SPIN、UV、SVE、HyTech、Kronos等；行為一致檢驗工具有FDR、Cospan/Formal Check等；復(fù)合檢驗工具有HSIS、VIS、STeP、METAFrame等。模型檢測實例貝爾實驗室對其高級數(shù)據(jù)鏈路控制器在FormalCheck下進行了模型檢驗功能驗證，6個性能進行了規(guī)格，其中5個驗證無誤、另外一個失敗，從而進一步發(fā)現(xiàn)了一個影響信道流量的Bug；1019數(shù)目的狀態(tài)。經(jīng)過模型檢驗分析發(fā)現(xiàn)了影響主動控制效果的計時器設(shè)置錯誤；-45-（2）形式化驗證模型檢測實例基于SMV輸入語言建立了標準下cache一致協(xié)議的精確模型，通過SMV驗證

34、了模型滿足cache一致性的規(guī)格。并發(fā)現(xiàn)了先前并未找到的潛在協(xié)議設(shè)計錯誤。該工作是第一次從IEEE標準中發(fā)現(xiàn)錯誤；Philips公司音響設(shè)備的控制協(xié)議通過HyTech得到了完全自動驗證，這是一個具有離散和連續(xù)特征的混雜系統(tǒng)驗證問題；AT&T公司的7500條通信軟件的SDL源代碼進行了驗證，從中發(fā)現(xiàn)112個錯誤，約55的初始設(shè)計需求在邏輯上不一致。-46-（2）形式化驗證定理證明采用邏輯公式來規(guī)格系統(tǒng)及其性質(zhì)，其中的邏輯由一個具有公理和推理規(guī)則的形式化系統(tǒng)給出，進行定理證明的過程就是應(yīng)用這些公理或推理規(guī)則來證明系統(tǒng)具有某些性質(zhì)。不同于模型檢驗，定理證明可以處理無限狀態(tài)空間問題。定理證明系統(tǒng)又可以

35、粗略地分為自動和交互式兩種類型。自動定理證明系統(tǒng)是通用搜索過程，在解決各種組合問題中比較成功；交互式定理證明系統(tǒng)需要與用戶進行交互，要求用戶能提供驗證中創(chuàng)造性最強部分（建立斷言等）的工作，因而其效率較低，較難用于大系統(tǒng)的驗證。-47-（2）形式化驗證定理證明工具用戶導(dǎo)引自動推演工具有ACL2、Eves、LP、Nqthm、Reve和RRL；證明檢驗器有Coq、HOL、LEGO、LCF和Nuprl；復(fù)合證明器Analytica、PVS和Step；定理證明實例基于符號代數(shù)運算的自動定理證明用于證明Pentium中SRT算法的正確性，檢查出了一個由故障商數(shù)字選擇表引起的錯誤；-48-（2）形式化驗證定

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

37、108條進行了規(guī)格，驗證了11個有代表性的微代碼。-49-（3）程序求精程序求精，又稱為程序變換，是將自動推理和形式化方法相結(jié)合而形成的一門新技術(shù)，它研究從抽象的形式規(guī)格推演出具體的面向計算機的程序代碼的全過程。程序求精的基本思想是用一個抽象程度低、過程性強的程序去代替一個抽象程度高、過程性弱的程序，并保持它們之間功能的一致。這里所說的“程序”與傳統(tǒng)觀點中“可以由計算機直接執(zhí)行”的“程序”不同，這里的“程序”是對規(guī)格、設(shè)計文檔以及程序代碼的統(tǒng)稱。在這種理解下，程序可以劃分為若干層次：最高層是不能直接執(zhí)行的程序，即規(guī)格，它由抽象的描述語句構(gòu)成；最低層是可以直接執(zhí)行的程序，稱為程序代碼，它由可執(zhí)行的命令語句構(gòu)成；最高層和最低層之間為一系列混合程序，其中既含有抽象的描述語句，又含有可執(zhí)行的命令語句。 -50-