形式化方法引論

形式化方法引論第1頁，共72頁，2023年，2月20日，星期六目錄單擊此處添加標題文字單擊此處添加文字內(nèi)容單擊此處添加文字內(nèi)容單擊此處添加文字內(nèi)容1單擊此處添加標題文字單擊此處添加文字內(nèi)容單擊此處添加文字內(nèi)容單擊此處添加文字內(nèi)容2單擊此處添加標題文字單擊此處添加文字內(nèi)容單擊此處添加文字內(nèi)容單擊此處添加文字內(nèi)容3單擊此處添加標題文字單擊此處添加文字內(nèi)容單擊此處添加文字內(nèi)容單擊此處添加文字內(nèi)容4第2頁，共72頁，2023年，2月20日，星期六形式化方法形式化方法(formalmethods)

在邏輯科學中是指分析、研究思維形式結(jié)構(gòu)的方法。它能精確地揭示各種邏輯規(guī)律,制定相應的邏輯規(guī)則,使各種理論體系更加嚴密。也能正確地訓練思維、提高思維的抽象能力。第3頁，共72頁，2023年，2月20日，星期六軟件工程方法的一種分類軟件工程方法可以按照在軟件開發(fā)中應用數(shù)學的嚴格程度（即形式化程度），進行分類。完全非形式化的方法：指運用圖、文本、表格和簡單符號等，去建立各種軟件模型。其中不使用數(shù)學。完全形式化的方法：以具有良好數(shù)學基礎和數(shù)學表示形式的形式化規(guī)格語言，建立各種軟件模型。第4頁，共72頁，2023年，2月20日，星期六完全非形式化的方法的缺陷各種模型中很容易包含具有矛盾、歧義、含糊、不完整的內(nèi)容。也容易產(chǎn)生抽象程度的混雜。第5頁，共72頁，2023年，2月20日，星期六形式化方法的優(yōu)點形式化方法支持抽象，利于建模形式化方法是準確的，利于減除模糊和歧義形式化方法是精確的，利于提高簡潔和清晰形式化方法是嚴格的，利于提高正確性形式化方法支持推理，利于檢測矛盾和不完整形式化方法能夠提供高層的描述和驗證手段第6頁，共72頁，2023年，2月20日，星期六形式化方法(FormalMethod)的基本含義是借助數(shù)學的方法來研究計算機科學中的有關問題。定義：“用于開發(fā)計算機系統(tǒng)的形式化方法是基于數(shù)學的用于描述系統(tǒng)性質(zhì)的技術。這樣的形式化方法提供了一個框架，人們可以在該框架中以系統(tǒng)的方式刻畫、開發(fā)和驗證系統(tǒng)”。

第7頁，共72頁，2023年，2月20日，星期六軟件形式化方法的定義軟件形式化方法基于良好的數(shù)學基礎，提供了一個框架，在框架中可以用系統(tǒng)的而不是特別的方式刻劃、開發(fā)和驗證軟件系統(tǒng)。形式化方法的本質(zhì)是基于數(shù)學的方法來描述目標軟件系統(tǒng)屬性不同的形式化方法的數(shù)學基礎是不同的有的以集合論和一階謂詞演算為基礎（如Z和VDM）有的以時態(tài)邏輯為基礎數(shù)學基礎提供了一系列精確定義的概念一致性完整性正確性形式化方法需要形式化規(guī)約說明語言的支持第8頁，共72頁，2023年，2月20日，星期六在軟件開發(fā)的全過程中，凡是采用嚴格的數(shù)學語言，具有精確的數(shù)學語義的方法，都稱為形式化方法。從廣義角度，形式化方法是軟件開發(fā)過程中分析、設計及實現(xiàn)的系統(tǒng)工程方法。從狹義角度，形式化方法是軟件規(guī)格(Specification)和驗證(Verification)的方法。因此，形式化方法又分為形式化規(guī)格方法和形式化驗證方法。第9頁，共72頁，2023年，2月20日，星期六形式化規(guī)格是通過具有明確數(shù)學定義的文法和語義的方法或語言對軟件的期望特性或者行為進行的精確、簡潔描述。形式化驗證是基于已建立的形式化規(guī)格，對軟件的相關特性進行評價的數(shù)學分析和證明。第10頁，共72頁，2023年，2月20日，星期六形式化方法的發(fā)展軟件的形式化開發(fā)方法，最早可追溯到20世紀50年代后期對程序設計語言編譯技術的研究。出現(xiàn)了形式化說明和驗證編譯程序的各種方法J.Backus提出BNF描述Algol60語言的語法出現(xiàn)了各種語法分析程序自動生成器以及語法制導的編譯方法，使得編譯系統(tǒng)的開發(fā)從“手工藝制作方式”發(fā)展成具有牢固理論基礎的系統(tǒng)方法。第11頁，共72頁，2023年，2月20日，星期六形式化方法的發(fā)展在20世紀60年代，面對當時出現(xiàn)的軟件危機，F(xiàn)loyd、Hoare和Manna等開展的程序正確性證明研究推動了形式化方法的發(fā)展，他們試圖用數(shù)學方法來證明程序的正確性并發(fā)展成為了各種程序驗證方法，但是受程序規(guī)模的限制，這些方法并未達到預期的應用效果。第12頁，共72頁，2023年，2月20日，星期六形式化方法的發(fā)展20世紀80年代，在硬件設計領域形式化方法的工業(yè)應用結(jié)果掀起了軟件形式化開發(fā)方法的學術研究和工業(yè)應用的熱潮。Pnueh提出了反應式系統(tǒng)規(guī)格和驗證的時態(tài)邏輯（TemporalLogic，TL）方法。Clarke和Emerson提出了有窮狀態(tài)并發(fā)系統(tǒng)的模型檢驗(ModelChecking)方法。第13頁，共72頁，2023年，2月20日，星期六形式化方法的發(fā)展經(jīng)過幾十年的研究和應用，形式化方法取得了大量、重要的成果從早期最簡單的形式化方法——一階謂詞演算方法到現(xiàn)在的應用于不同領域、不同階段的基于邏輯、狀態(tài)機、網(wǎng)絡、進程代數(shù)、代數(shù)等眾多形式化方法形式化方法逐漸融入軟件開發(fā)過程的各個階段,從需求分析、功能描述(規(guī)約)、(體系結(jié)構(gòu)/算法)設計、編程、測試直至維護。第14頁，共72頁，2023年，2月20日，星期六形式化方法的發(fā)展近年來，形式化方法的研究及其在工業(yè)中的應用得到了長足的發(fā)展。研究人員建立了系統(tǒng)設計人員易于理解的規(guī)格概念和術語，以及有效應用這些術語和概念的形式化規(guī)格方法及語言，建立了功能更加強大和完善的模型檢驗和定理證明技術。開發(fā)出了與之相應的從研究原型到商品化產(chǎn)品的支撐工具和環(huán)境。第15頁，共72頁，2023年，2月20日，星期六將形式化方法用于軟件開發(fā)的主要目的是保證軟件的正確性。形式化方法基于嚴格的數(shù)學，而在軟件開發(fā)過程中使用數(shù)學具有如下優(yōu)點：數(shù)學是準確的建模媒體，能夠?qū)ΜF(xiàn)象、對象、動作等進行簡潔、準確地描述。數(shù)學支持抽象，它使得規(guī)格的本質(zhì)可以被展示出來，并且還可以以一種有組織的方式來表示系統(tǒng)規(guī)格中的抽象層次。數(shù)學提供了高層確認的手段，可以使用數(shù)學證明，來揭示規(guī)格中的矛盾性和不完整性，以及用來展示設計和規(guī)格之間的一致情況等。第16頁，共72頁，2023年，2月20日，星期六形式化規(guī)格說明涉及的主要概念形式化方法為系統(tǒng)的數(shù)據(jù)和功能，定義了數(shù)據(jù)不變式、狀態(tài)和操作。數(shù)據(jù)不變式一組條件表達式，每個條件在包含一組數(shù)據(jù)的系統(tǒng)的執(zhí)行過程中總應保持為真狀態(tài)是從系統(tǒng)的外部能夠觀察到的行為模式的一種表示，或者是系統(tǒng)訪問和修改的存儲數(shù)據(jù)操作系統(tǒng)中發(fā)生的動作，以及對狀態(tài)數(shù)據(jù)的讀寫。第17頁，共72頁，2023年，2月20日，星期六形式化規(guī)格說明涉及的主要概念與操作相關的三種類型的條件不變式前置條件：定義操作執(zhí)行前須滿足的前提條件后置條件：定義操作執(zhí)行后需滿足的條件。通過定義操作對數(shù)據(jù)影響效果的方式來表達第18頁，共72頁，2023年，2月20日，星期六形式化軟件開發(fā)方法采用了軟件生命周期的變換模型。從某種角度上，形式化軟件開發(fā)方法實際上就是把現(xiàn)實世界的需求反映成軟件的模型化過程。在進行模型化的過程中涉及到三方面的系統(tǒng)模型現(xiàn)實世界模型表示計算機系統(tǒng)第19頁，共72頁，2023年，2月20日，星期六形式化軟件開發(fā)方法的過程就是從這三方面對系統(tǒng)進行描述和轉(zhuǎn)換的過程。開發(fā)過程中的任務依次分為模型獲取模型驗證模型變換第20頁，共72頁，2023年，2月20日，星期六模型獲取是從現(xiàn)實世界向模型表示轉(zhuǎn)換的過程，包括如何提取出模型以及如何表示模型，它對應于軟件生命周期中的需求分析、規(guī)格，以及設計等活動。模型驗證是對所得到的模型表示進行檢驗，判斷其是否捕獲了所有的用戶需求，以及該模型是否具有所期望的特性。第21頁，共72頁，2023年，2月20日，星期六模型變換是從模型表示向計算機系統(tǒng)變換的過程，一個抽象的模型表示可以變換到各種計算機系統(tǒng)環(huán)境上。模型變換對應于軟件生命周期中的實現(xiàn)和測試等活動。這些任務分別對應于如下三方面的活動：形式化規(guī)格形式化驗證程序求精(Refinement)在模型變換時的一個關鍵任務是進行一致性測試。即判斷在變換后所得到的計算機系統(tǒng)是否與模型表示相一致。第22頁，共72頁，2023年，2月20日，星期六形式規(guī)約形式規(guī)約(FormalSpecification,也稱形式規(guī)范或形式化描述)它是對程序“做什么”(whattodo)的數(shù)學描述,是用具有精確語義的形式語言書寫的程序功能描述,它是設計和編制程序的出發(fā)點,也是驗證程序是否正確的依據(jù)。對形式規(guī)約通常要討論其一致性(自身無矛盾)和完備性(是否完全、無遺漏地刻畫所要描述的對象)等性質(zhì)。第23頁，共72頁，2023年，2月20日，星期六形式規(guī)約形式規(guī)約的方法主要可分為兩類:一類是面向模型的方法也稱為系統(tǒng)建模,該方法通過構(gòu)造系統(tǒng)的計算模型來刻畫系統(tǒng)的不同行為特征；另一類是面向性質(zhì)的方法也稱為性質(zhì)描述,該方法通過定義系統(tǒng)必須滿足的一些性質(zhì)來描述一個系統(tǒng)。第24頁，共72頁，2023年，2月20日，星期六形式規(guī)約不同的形式規(guī)約方法要求不同的形式規(guī)約語言,即用于書寫形式規(guī)約的語言(也稱形式化描述語言),代數(shù)語言OBJ、Clear、ASL、ACTOne/Two等進程代數(shù)語言CSP、CCS、π演算等；時序邏輯語言PLTL、CTL、XYZ/E、UNITY、TLA等；這些規(guī)約語言由于基于不同的數(shù)學理論及規(guī)約方法，因而也千差萬別，但它們有一個共同的特點,即每種規(guī)約語言均由基本成分和構(gòu)造成分兩部分構(gòu)成。前者用來描述基本(原子)規(guī)約,后者把基本部分組合成大規(guī)約。構(gòu)造成分是形式規(guī)約研究和設計的重點，也是衡量規(guī)約語言優(yōu)劣的主要依據(jù)。第25頁，共72頁，2023年，2月20日，星期六一個簡化的生命周期模型定義軟件需求文檔SRD在完成需求搜集和分析之后，得到了軟件需求文檔SRD。它可被當作客戶與軟件提供者之間的合同。定義軟件需求規(guī)格或行為規(guī)格(BS)軟件需求規(guī)格（或行為規(guī)格）在不去考慮系統(tǒng)的具體實現(xiàn)方法的前提下，描述了系統(tǒng)所期望的是什么。它以SRD中所聲明的對象為基礎，根據(jù)從外部可觀察到的系統(tǒng)功能特征，來對所期望的系統(tǒng)行為進行準確和明確的描述。如果存在對系統(tǒng)的約束，也可將其作為系統(tǒng)的特征來進行說明。第26頁，共72頁，2023年，2月20日，星期六一個簡化的生命周期模型定義設計規(guī)格(DS)設計規(guī)格在保持需求規(guī)格所聲明的特征的前提下，指明系統(tǒng)的運行特點和內(nèi)部結(jié)構(gòu)。并可能根據(jù)一些具體需要，提供實現(xiàn)其行為的機制。設計規(guī)格與行為規(guī)格相比，增加了更多的細節(jié)。然而必須確保這些細節(jié)不改變需求規(guī)格所定義的系統(tǒng)的外部行為。通過增加越來越多的數(shù)據(jù)、行為、控制，以及異常描述等方面的細節(jié)，設計規(guī)格細化軟件需求規(guī)格，并對需求規(guī)格進行更具體地描述。第27頁，共72頁，2023年，2月20日，星期六一個簡化的生命周期模型對于設計規(guī)格中的每一個組件，可以更加詳細地指定組件的界面和組件間的交互，并進一步細化成一系列的規(guī)格。從而得到界面規(guī)格和詳細設計規(guī)格或程序規(guī)格(PS)。詳細設計規(guī)格可以用程序來實現(xiàn)。第28頁，共72頁，2023年，2月20日，星期六規(guī)格可以采用非形式化的方式描述，包括自然語言、圖、表等，也可以采用形式化方式描述。由于非形式化方法本身所存在的矛盾、二義性、含糊性，以及描述規(guī)格時的不完整性、抽象層次混雜等情況，使得所得到的規(guī)格不能準確地刻畫系統(tǒng)模型，甚至會為后來的軟件開發(fā)埋下出錯的隱患。第29頁，共72頁，2023年，2月20日，星期六形式化方法由于基于嚴格的數(shù)學基礎，具有嚴格的語法和語義定義，從而可以準確地描述系統(tǒng)模型，排除了矛盾、二義性、含糊性等情況。在對系統(tǒng)進行嚴格地描述的過程中，將會幫助開發(fā)人員和用戶明確那些原本模糊的需求，并發(fā)現(xiàn)用戶所陳述的需求中存在的矛盾，有利于相對完整、正確地理解用戶需求，最終得到一個完整、正確的系統(tǒng)模型。第30頁，共72頁，2023年，2月20日，星期六形式化規(guī)格精確地描述了用戶的需求、軟件系統(tǒng)的功能以及各種性質(zhì)，其描述的是“做什么”，而不考慮“怎么做”。在書寫規(guī)格時應該注意的一個問題是：如何描述得恰如其分，既不過多也不過少。在規(guī)格中描述過多會導致“實現(xiàn)偏向”，給實現(xiàn)施加了不必要的限制，從而排除了一些原本是合理的實現(xiàn)。描述得過少又有容納不合理實現(xiàn)的危險。為了開發(fā)出良好的規(guī)格，除了應透徹理解、熟練掌握所使用的形式規(guī)格語言和方法外，還應對所要描述的系統(tǒng)有全面深入的了解。

第31頁，共72頁，2023年，2月20日，星期六已建立了多種適用于軟件系統(tǒng)規(guī)格的形式化方法，可分為三類：操作類描述類雙重類操作類方法基于狀態(tài)和轉(zhuǎn)移，通過可執(zhí)行模型來描述系統(tǒng)，模型本身能夠采用靜態(tài)分析和模型執(zhí)行而得到驗證，這類方法包括有限狀態(tài)機、Statecharts、Petri網(wǎng)等。第32頁，共72頁，2023年，2月20日，星期六描述類方法基于數(shù)學公理和概念，通過邏輯或代數(shù)給出系統(tǒng)的狀態(tài)空間，具有高度抽象的特點，便于通過自動工具進行驗證?；诓煌臄?shù)學基礎，描述類方法進一步分為：基于代數(shù)的描述類方法，如Z、VDM、Larch等?；谶壿嫷拿枋鲱惙椒ǎ缑}線性時態(tài)邏輯(PropositionalLinearTemporalLogic，PLTL)一階線性時態(tài)邏輯(First—OrderLinearTernporalLogic，PLTL)計算樹邏輯(ComputationTreeTemporalLogic，CTTL)等時態(tài)邏輯為代表第33頁，共72頁，2023年，2月20日，星期六雙重類方法則兼有前面二者的特點，既能夠通過數(shù)學公理和概念來高度抽象地描述系統(tǒng)，又具有狀態(tài)和轉(zhuǎn)移的可執(zhí)行特征。這類方法包括：擴展狀態(tài)機／實時時態(tài)邏輯(ExtendedStateMachine／Real一TimeTemporalLogic，ESM／RTTL)TRIO+TROL等第34頁，共72頁，2023年，2月20日，星期六20世紀80年代，牛津大學和Hursley實驗室合作將Z方法，用于開發(fā)IBM商用信息控制系統(tǒng)。IBM對整個開發(fā)所進行的測試表明：明顯地改善了產(chǎn)品質(zhì)量大量地減少了錯誤和早期診斷錯誤其總體開發(fā)成本降低了9％（IBM估計）這一成果榮獲皇家技術成就獎第35頁，共72頁，2023年，2月20日，星期六Praxis公司于1992年開發(fā)了英國民航局的信息顯示系統(tǒng)倫敦機場新空中交通管理系統(tǒng)的一部分在該系統(tǒng)的需求分析階段，形式化規(guī)格和非形式結(jié)構(gòu)化的需求概念相結(jié)合。在系統(tǒng)規(guī)格階段，采用了抽象的VDM模型。在設計階段，抽象VDM模型被細化為更具體的模塊化規(guī)格。第36頁，共72頁，2023年，2月20日，星期六Praxis公司這個項目開發(fā)的生產(chǎn)效率與采用非形式化技術相當、甚至更好。軟件質(zhì)量得到了很大的提高軟件的故障率僅為0.75每千行代碼，大大低于采用非形式化技術所開發(fā)出的軟件系統(tǒng)的故障率（約為2～20每千行代碼）第37頁，共72頁，2023年，2月20日，星期六美國加州大學的安全關鍵系統(tǒng)研究組所開發(fā)的空中交通防碰撞系統(tǒng)的形式化需求規(guī)格TCASII，采用了基于Statecharts的需求狀態(tài)機語言RSML，解決了開發(fā)過程中遇到的許多問題。TCASH項目表明復雜過程控制系統(tǒng)軟件開發(fā)采用形式化需求規(guī)格的可能性應用工程師們不經(jīng)任何專門培訓建立易讀且易評判的形式化規(guī)格的可行性（注：Statecharts相對容易）第38頁，共72頁，2023年，2月20日，星期六形式化規(guī)格還在如下方面得到了應用數(shù)據(jù)庫：用于存儲病人監(jiān)護信息的HP醫(yī)用儀器實時數(shù)據(jù)庫系統(tǒng)電子儀器：Tektronix系列諧波發(fā)生器、Schlumberger家用電度計硬件：INMOS浮點處理器、INMOS中T9000系列的虛擬信道處理器醫(yī)療設備：核磁共振理療系統(tǒng)核反應堆系統(tǒng)：核反應器安全系統(tǒng)、核發(fā)電系統(tǒng)的切換裝置第39頁，共72頁，2023年，2月20日，星期六形式化規(guī)格還在如下方面得到了應用保密系統(tǒng)：NATO控制指揮和控制系統(tǒng)中的保密策略模型、Multinet網(wǎng)關系統(tǒng)的數(shù)據(jù)安全傳輸、美國國家標準和技術院的令牌訪問控制系統(tǒng)電信系統(tǒng)：AT&T的5ESS電話交換系統(tǒng)、德國電信的電話業(yè)務系統(tǒng)運輸系統(tǒng)：巴黎地鐵的自動火車保護系統(tǒng)、英國鐵路信號控制、以色列機載航空電子軟件。第40頁，共72頁，2023年，2月20日，星期六形式化驗證軟件開發(fā)中的絕大部分錯誤是在需求分析和規(guī)格的早期階段引入的，這些錯誤將隨著開發(fā)的深入而逐漸放大。并且，這些錯誤發(fā)現(xiàn)得越晚，對其修改所需付出的代價也將會越大。在傳統(tǒng)的軟件開發(fā)方法中，除了在各個開發(fā)階段進行評審以發(fā)現(xiàn)錯誤外，更多的錯誤則是直到編碼結(jié)束后的測試階段才能被檢測出。形式化方法在開發(fā)出形式規(guī)格后就進行形式驗證。實際上是使得驗證工作得以提前進行，既可以提前發(fā)現(xiàn)錯誤，同時在修改所發(fā)現(xiàn)的錯誤時需要付出的代價也是最小的。第41頁，共72頁，2023年，2月20日，星期六形式化驗證形式化驗證的主要技術包括模型檢驗和定理證明模型檢驗是一種基于有限狀態(tài)模型并檢驗該模型的期望特性的技術。模型檢驗就是對模型的狀態(tài)空間進行蠻力搜索，以確認該系統(tǒng)模型是否具有某些性質(zhì)。搜索的可終止性依賴于模型的有限性。模型檢驗主要適用于有窮狀態(tài)系統(tǒng)。第42頁，共72頁，2023年，2月20日，星期六形式化驗證模型檢驗的優(yōu)點完全自動化并且驗證速度快當所檢驗的性質(zhì)未被滿足時，將終止搜索過程并給出反例。這種信息常常反映了系統(tǒng)設計中的失誤，因而對于用戶排錯有極大的幫助。模型檢驗可用于系統(tǒng)的部分規(guī)格，即對于只給出了部分規(guī)格的系統(tǒng)，通過搜索也可以提供關于已知部分正確性的有用信息。第43頁，共72頁，2023年，2月20日，星期六形式化驗證模型檢驗方法的一個嚴重缺陷是“狀態(tài)爆炸問題”。即，隨著所要檢驗的系統(tǒng)的規(guī)模增大，模型檢驗算法所需的時間／空間開銷往往呈指數(shù)增長，因而極大地限制了其實際使用范圍。有序二叉決策圖(OrderedBinaryDecisionDiagrams，OBDD)是表述狀態(tài)轉(zhuǎn)移系統(tǒng)的高效率方法，使得較大規(guī)模系統(tǒng)的驗證成為可能。模型檢驗可以處理100至200個狀態(tài)變量的系統(tǒng)。模型檢驗已用來檢驗狀態(tài)數(shù)目可達10120的系統(tǒng)。并且通過采用適當?shù)某橄蠹夹g，就可以處理具有更多狀態(tài)的系統(tǒng)。第44頁，共72頁，2023年，2月20日，星期六形式化驗證模型檢驗離不開模型檢驗工具的支持。已有的模型檢驗工具可分為時態(tài)邏輯模型檢驗工具行為一致檢驗工具復合檢驗工具。時態(tài)邏輯模型檢驗工具有EMC、CESAR、SMV、Murphi、SPIN、UV、SVE、HyTech、Kronos等行為一致檢驗工具有Cospan／FormalllCheck、FDR等；復合檢驗工具有HSIS、VIS、STeP、METAFrame等。第45頁，共72頁，2023年，2月20日，星期六形式化驗證貝爾實驗室在FormalCheck下，對其高級數(shù)據(jù)鏈路控制器進行了模型檢驗，以驗證功能。他們對6個性能進行了規(guī)格，其中5個驗證無誤，另外一個失敗，從而進一步發(fā)現(xiàn)了一個影響信道流量的Bug。樓宇抗震分布式主動結(jié)構(gòu)控制系統(tǒng)的設計規(guī)格的系統(tǒng)模型有2.12×1019數(shù)目的狀態(tài)。經(jīng)過模型檢驗，自動分析并發(fā)現(xiàn)了影響主動控制效果的計時器設置錯誤。第46頁，共72頁，2023年，2月20日，星期六形式化驗證基于SMV輸入語言建立了IEEEFuturebus+896.1一1991標準下cache一致協(xié)議的精確模型，通過SMV驗證了轉(zhuǎn)移系統(tǒng)模型滿足cache一致性的規(guī)格。從中發(fā)現(xiàn)了先前并未找到和潛在的協(xié)議設計中的錯誤。Murphi有限狀態(tài)模型檢驗工具對IEEE標準1596一1992下cache一致協(xié)議進行了驗證，發(fā)現(xiàn)了變量、邏輯等方面的錯誤。第47頁，共72頁，2023年，2月20日，星期六形式化驗證Philips公司音響設備的控制協(xié)議通過HyTech得到了完全自動驗證，這是一個具有離散和連續(xù)特征的混雜系統(tǒng)的驗證問題。對AT&T公司的7500條通信軟件的SDL源代碼進行了驗證，從中發(fā)現(xiàn)112個錯誤，約55％的初始設計需求在邏輯上不一致。第48頁，共72頁，2023年，2月20日，星期六形式化驗證—定理證明定理證明采用邏輯公式來規(guī)格系統(tǒng)及其性質(zhì)。邏輯公式由一個具有公理和推理規(guī)則的形式化系統(tǒng)給出。進行定理證明的過程就是應用這些公理或推理規(guī)則來證明系統(tǒng)具有某些性質(zhì)。不同于模型檢驗，定理證明可以處理無限狀態(tài)空間問題。第49頁，共72頁，2023年，2月20日，星期六形式化驗證—定理證明定理證明系統(tǒng)可分為自動和交互式兩種類型。自動定理證明系統(tǒng)是通用搜索過程，在解決各種組合問題中比較成功。交互式定理證明系統(tǒng)需要與用戶進行交互，要求用戶能提供驗證中創(chuàng)造性最強部分(建立斷言等)的工作，因而其效率較低，較難用于大系統(tǒng)的驗證。第50頁，共72頁，2023年，2月20日，星期六形式化驗證—定理證明定理證明的的實施同樣需要定理證明器的支持?，F(xiàn)有的定理證明器包括：用戶導引自動推演工具證明檢驗器復合證明器第51頁，共72頁，2023年，2月20日，星期六形式化驗證—定理證明用戶導引自動推演工具有ACL2、Eves、LP、Nqthm、Reve和RRI這些工具由引理或者定義序列導引，每一個定理采用已建立的推演和引理，進行自動證明。證明檢驗器有Coq、HOL、LEGO、LCF和Nuprl復合證明器Analytica中將定理證明和符號代數(shù)系統(tǒng)Mathematica復合，PVS和Step將決策過程、模型檢驗和交互式證明復合在一體。第52頁，共72頁，2023年，2月20日，星期六形式化驗證—定理證明基于符號代數(shù)運算的自動定理證明用于證明Pentium中SRT算法的正確性，檢查出了一個錯誤。ACL2用于AMD5K86的浮點除微代碼的規(guī)格和機械證明，ACL2還用來檢驗浮點方根微的代碼的正確性，發(fā)現(xiàn)了其中的Bug，并對修改后的微代碼進行了正確性的機器證明。ACL2用于Motorola復數(shù)算術處理器CSP的完全規(guī)格，同時對CSP的幾個算法進行了驗證。PVS用于航空電子微處理器AAMP5的規(guī)格和驗證，對209條AAMP5指令中的108條進行了規(guī)格，驗證了11個有代表性的微代碼。第53頁，共72頁，2023年，2月20日，星期六程序求精程序求精又稱為程序變換，是將自動推理和形式化方法相結(jié)合而形成的一門技術。它研究從抽象的形式規(guī)格推演出具體的面向計算機的程序代碼的全過程。程序求精的基本思想是用一個抽象程度低、過程性強的程序去代替一個抽象程度高、過程性弱的程序，并保持它們之問功能的一致性。這里所說的“程序”與傳統(tǒng)觀點中“可以由計算機直接執(zhí)行”的“程序”不同，這里的“程序”是對規(guī)格、設計文檔，以及程序代碼的統(tǒng)稱。第54頁，共72頁，2023年，2月20日，星期六程序求精因此，“程序”可以劃分為若干層次最高層是不能直接執(zhí)行的程序，即規(guī)格，它由抽象的描述語句構(gòu)成。最低層是可以直接執(zhí)行的程序，稱為程序代碼，它由可執(zhí)行的命令語句構(gòu)成。最高層和最低層之間為一系列混合程序，其中既含有抽象的描述語句，又含有可執(zhí)行的命令語句。第55頁，共72頁，2023年，2月20日，星期六程序求精程序開發(fā)過程實際上就是從最高層的程序開始，通過一系列的求精變換步驟，每一步都降低一些抽象程度或增加一些可執(zhí)行性，最終得到能夠指導計算機明確執(zhí)行的程序代碼。在進行求精的過程中要注意保證程序的正確性，即保證所得到的程序是滿足最初的形式規(guī)格的。程序的這種正確性可以通過求精過程中所遵循的一系列規(guī)則來保證，也可以在事后采用驗證工具來證明。第56頁，共72頁，2023年，2月20日，星期六程序求精程序求精技術是形式化方法研究的一個熱點。在已出現(xiàn)的許多相關技術中，真正能夠應用到實際軟件開發(fā)過程中的并不多。目前比較典型的是IBMHursley公司和牛津大學PRG程序設計研究組提出的針對Z規(guī)格的求精方法，以及CarrollMogan的規(guī)則求精方案。

第57頁，共72頁，2023年，2月20日，星期六程序求精形式化開發(fā)方法一直受到多方面的爭議，這些爭議主要體現(xiàn)在：形式化方法中所包含的數(shù)學理論，限制了大多數(shù)程序設計人員的學習和使用。采用形式化方法會延誤項目開發(fā)周期，增加開發(fā)費用。許多流行的形式化方法對于較小規(guī)模項目是有效的，但卻很難應用于大型項目。形式化方法不能確保開發(fā)出完全正確的軟件缺乏對軟件生命周期內(nèi)各個階段提供全面支持的形式化方法等。

第58頁，共72頁，2023年，2月20日，星期六程序求精形式化方法中的抽象數(shù)學符號及理論確實給軟件工程師的使用帶來一些不便，以致于人們要花時間和精力去學習和掌握。但是，采用形式化方法可以極大地減少系統(tǒng)設計開發(fā)早期階段的錯誤，避免后期錯誤修改所帶來的高額成本開銷。采用形式化方法還會提高系統(tǒng)的開發(fā)效率。并且形式化方法是高質(zhì)量、高可靠性軟件開發(fā)的有效途徑，是軟件自動化的根本前提。第59頁，共72頁，2023年，2月20日，星期六程序求精形式化方法不會完全代替非形式化的軟件開發(fā)方法，軟件工程師們需要根據(jù)所解決問題的特點結(jié)合或選擇使用。第60頁，共72頁，2023年，2月20日，星期六程序求精形式化方法結(jié)合到具體的軟件開發(fā)過程中需要考慮如下一些因素：應用的類型：形式化方法不可能對所有的應用類型都適用。對于一個項目，應該衡量其問題領域的特點以及模型的復雜性，從而確定是否適于采用形式化方法。第61頁，共72頁，2023年，2月20日，星期六程序求精規(guī)模和結(jié)構(gòu)：在將形式化方法用于一個項目之前，還應該評價項目的規(guī)模和結(jié)構(gòu)復雜性。形式化方法可有效地適用于中等規(guī)模的系統(tǒng)。為了使大型系統(tǒng)能充分受益于所采用的形式化方法，該系統(tǒng)應該具有很好的結(jié)構(gòu)，并能分解成定義良好的構(gòu)件，從而使其中的關鍵部分只受形式化方法的控制。類型的選擇：在將形式化方法用于一個項目時，必須能清楚地確定其目標。不同的應用目的將對開發(fā)過程產(chǎn)生不同的影響，從而影響到對形式化方法類型的選擇。第62頁，共72頁，2023年，2月20日，星期六程序求精形式化級別：對一個系統(tǒng)可能進行非形式化、半形式化或者高度形式化的描述。從某個給定項目的目標出發(fā)，必須先確定其應用的關鍵程度、項目規(guī)模、可用的資源，以及對項目合適的形式化程度等，并從這些可能性中做出一個選擇。使用范圍：雖然形式化方法可使用于開發(fā)過程的所有階段，但通常只是有選擇地使用。一方面需要對形式化方法所應用于的開發(fā)階段進行選擇，另一方面，需要對采用形式化方法的構(gòu)件進行選擇。對那些決定安全性的構(gòu)件不但需要形式化，而且需要高度的形式化。第63頁，共72頁，2023年，2月20日，星期六程序求精工具：為了足夠精確地實施形式化方法，工具的支持是必須的。第64頁，共72頁，2023年，2月20日，星期六程序求精形式化方法在軟件產(chǎn)業(yè)中應用的深入有賴于諸多方面工作的進展。需要開發(fā)出將整體特性分解為易于驗證的局部特性的有效方法大規(guī)模復雜軟件中搜索空間是巨大的，需要研究新的處理方法形式化方法與非形式化方法的結(jié)合形式化方法和新的軟件開發(fā)技術（如SOA）的結(jié)合需要有效的軟件工具第65頁，共72頁，2023年，2