形式化方法引論

1、軟件開發(fā)的形式化方法引論,目錄,形式化方法,形式化方法(formalmethods)在邏輯科學(xué)中是指分析、研究思維形式結(jié)構(gòu)的方法。它能精確地揭示各種邏輯規(guī)律,制定相應(yīng)的邏輯規(guī)則,使各種理論體系更加嚴(yán)密。也能正確地訓(xùn)練思維、提高思維的抽象能力。,軟件工程方法的一種分類,軟件工程方法可以按照在軟件開發(fā)中應(yīng)用數(shù)學(xué)的嚴(yán)格程度（即形式化程度），進(jìn)行分類。完全非形式化的方法：指運(yùn)用圖、文本、表格和簡單符號等，去建立各種軟件模型。其中不使用數(shù)學(xué)。完全形式化的方法：以具有良好數(shù)學(xué)基礎(chǔ)和數(shù)學(xué)表示形式的形式化規(guī)格語言，建立各種軟件模型。,完全非形式化的方法的缺陷,各種模型中很容易包含具有矛盾、歧義、含糊、不完整的

2、內(nèi)容。也容易產(chǎn)生抽象程度的混雜。,形式化方法的優(yōu)點(diǎn),形式化方法支持抽象，利于建模形式化方法是準(zhǔn)確的，利于減除模糊和歧義形式化方法是精確的，利于提高簡潔和清晰形式化方法是嚴(yán)格的，利于提高正確性形式化方法支持推理，利于檢測矛盾和不完整形式化方法能夠提供高層的描述和驗(yàn)證手段,形式化方法(FormalMethod)的基本含義是借助數(shù)學(xué)的方法來研究計算機(jī)科學(xué)中的有關(guān)問題。定義：“用于開發(fā)計算機(jī)系統(tǒng)的形式化方法是基于數(shù)學(xué)的用于描述系統(tǒng)性質(zhì)的技術(shù)。這樣的形式化方法提供了一個框架，人們可以在該框架中以系統(tǒng)的方式刻畫、開發(fā)和驗(yàn)證系統(tǒng)”。,軟件形式化方法的定義,軟件形式化方法基于良好的數(shù)學(xué)基礎(chǔ)，提供了一個框架，在

3、框架中可以用系統(tǒng)的而不是特別的方式刻劃、開發(fā)和驗(yàn)證軟件系統(tǒng)。形式化方法的本質(zhì)是基于數(shù)學(xué)的方法來描述目標(biāo)軟件系統(tǒng)屬性不同的形式化方法的數(shù)學(xué)基礎(chǔ)是不同的有的以集合論和一階謂詞演算為基礎(chǔ)（如Z和VDM）有的以時態(tài)邏輯為基礎(chǔ)數(shù)學(xué)基礎(chǔ)提供了一系列精確定義的概念一致性完整性正確性形式化方法需要形式化規(guī)約說明語言的支持,在軟件開發(fā)的全過程中，凡是采用嚴(yán)格的數(shù)學(xué)語言，具有精確的數(shù)學(xué)語義的方法，都稱為形式化方法。從廣義角度，形式化方法是軟件開發(fā)過程中分析、設(shè)計及實(shí)現(xiàn)的系統(tǒng)工程方法。從狹義角度，形式化方法是軟件規(guī)格(Specification)和驗(yàn)證(Verification)的方法。因此，形式化方法又分為形式化

4、規(guī)格方法和形式化驗(yàn)證方法。,形式化規(guī)格是通過具有明確數(shù)學(xué)定義的文法和語義的方法或語言對軟件的期望特性或者行為進(jìn)行的精確、簡潔描述。形式化驗(yàn)證是基于已建立的形式化規(guī)格，對軟件的相關(guān)特性進(jìn)行評價的數(shù)學(xué)分析和證明。,形式化方法的發(fā)展,軟件的形式化開發(fā)方法，最早可追溯到20世紀(jì)50年代后期對程序設(shè)計語言編譯技術(shù)的研究。出現(xiàn)了形式化說明和驗(yàn)證編譯程序的各種方法J.Backus提出BNF描述Algol60語言的語法出現(xiàn)了各種語法分析程序自動生成器以及語法制導(dǎo)的編譯方法，使得編譯系統(tǒng)的開發(fā)從“手工藝制作方式”發(fā)展成具有牢固理論基礎(chǔ)的系統(tǒng)方法。,形式化方法的發(fā)展,在20世紀(jì)60年代，面對當(dāng)時出現(xiàn)的軟件危機(jī)，F(xiàn)

5、loyd、Hoare和Manna等開展的程序正確性證明研究推動了形式化方法的發(fā)展，他們試圖用數(shù)學(xué)方法來證明程序的正確性并發(fā)展成為了各種程序驗(yàn)證方法，但是受程序規(guī)模的限制，這些方法并未達(dá)到預(yù)期的應(yīng)用效果。,形式化方法的發(fā)展,20世紀(jì)80年代，在硬件設(shè)計領(lǐng)域形式化方法的工業(yè)應(yīng)用結(jié)果掀起了軟件形式化開發(fā)方法的學(xué)術(shù)研究和工業(yè)應(yīng)用的熱潮。Pnueh提出了反應(yīng)式系統(tǒng)規(guī)格和驗(yàn)證的時態(tài)邏輯（TemporalLogic，TL）方法。Clarke和Emerson提出了有窮狀態(tài)并發(fā)系統(tǒng)的模型檢驗(yàn)(ModelChecking)方法。,形式化方法的發(fā)展,經(jīng)過幾十年的研究和應(yīng)用，形式化方法取得了大量、重要的成果從早期最簡

6、單的形式化方法一階謂詞演算方法到現(xiàn)在的應(yīng)用于不同領(lǐng)域、不同階段的基于邏輯、狀態(tài)機(jī)、網(wǎng)絡(luò)、進(jìn)程代數(shù)、代數(shù)等眾多形式化方法形式化方法逐漸融入軟件開發(fā)過程的各個階段,從需求分析、功能描述(規(guī)約)、(體系結(jié)構(gòu)/算法)設(shè)計、編程、測試直至維護(hù)。,形式化方法的發(fā)展,近年來，形式化方法的研究及其在工業(yè)中的應(yīng)用得到了長足的發(fā)展。研究人員建立了系統(tǒng)設(shè)計人員易于理解的規(guī)格概念和術(shù)語，以及有效應(yīng)用這些術(shù)語和概念的形式化規(guī)格方法及語言，建立了功能更加強(qiáng)大和完善的模型檢驗(yàn)和定理證明技術(shù)。開發(fā)出了與之相應(yīng)的從研究原型到商品化產(chǎn)品的支撐工具和環(huán)境。,將形式化方法用于軟件開發(fā)的主要目的是保證軟件的正確性。形式化方法基于嚴(yán)格的

7、數(shù)學(xué)，而在軟件開發(fā)過程中使用數(shù)學(xué)具有如下優(yōu)點(diǎn)：數(shù)學(xué)是準(zhǔn)確的建模媒體，能夠?qū)ΜF(xiàn)象、對象、動作等進(jìn)行簡潔、準(zhǔn)確地描述。數(shù)學(xué)支持抽象，它使得規(guī)格的本質(zhì)可以被展示出來，并且還可以以一種有組織的方式來表示系統(tǒng)規(guī)格中的抽象層次。數(shù)學(xué)提供了高層確認(rèn)的手段，可以使用數(shù)學(xué)證明，來揭示規(guī)格中的矛盾性和不完整性，以及用來展示設(shè)計和規(guī)格之間的一致情況等。,形式化規(guī)格說明涉及的主要概念,形式化方法為系統(tǒng)的數(shù)據(jù)和功能，定義了數(shù)據(jù)不變式、狀態(tài)和操作。數(shù)據(jù)不變式一組條件表達(dá)式，每個條件在包含一組數(shù)據(jù)的系統(tǒng)的執(zhí)行過程中總應(yīng)保持為真狀態(tài)是從系統(tǒng)的外部能夠觀察到的行為模式的一種表示，或者是系統(tǒng)訪問和修改的存儲數(shù)據(jù)操作系統(tǒng)中發(fā)生的動

8、作，以及對狀態(tài)數(shù)據(jù)的讀寫。,形式化規(guī)格說明涉及的主要概念,與操作相關(guān)的三種類型的條件不變式前置條件：定義操作執(zhí)行前須滿足的前提條件后置條件：定義操作執(zhí)行后需滿足的條件。通過定義操作對數(shù)據(jù)影響效果的方式來表達(dá),形式化軟件開發(fā)方法采用了軟件生命周期的變換模型。從某種角度上，形式化軟件開發(fā)方法實(shí)際上就是把現(xiàn)實(shí)世界的需求反映成軟件的模型化過程。在進(jìn)行模型化的過程中涉及到三方面的系統(tǒng)模型現(xiàn)實(shí)世界模型表示計算機(jī)系統(tǒng),形式化軟件開發(fā)方法的過程就是從這三方面對系統(tǒng)進(jìn)行描述和轉(zhuǎn)換的過程。開發(fā)過程中的任務(wù)依次分為模型獲取模型驗(yàn)證模型變換,模型獲取是從現(xiàn)實(shí)世界向模型表示轉(zhuǎn)換的過程，包括如何提取出模型以及如何表示模型

9、，它對應(yīng)于軟件生命周期中的需求分析、規(guī)格，以及設(shè)計等活動。模型驗(yàn)證是對所得到的模型表示進(jìn)行檢驗(yàn)，判斷其是否捕獲了所有的用戶需求，以及該模型是否具有所期望的特性。,模型變換是從模型表示向計算機(jī)系統(tǒng)變換的過程，一個抽象的模型表示可以變換到各種計算機(jī)系統(tǒng)環(huán)境上。模型變換對應(yīng)于軟件生命周期中的實(shí)現(xiàn)和測試等活動。這些任務(wù)分別對應(yīng)于如下三方面的活動：形式化規(guī)格形式化驗(yàn)證程序求精(Refinement)在模型變換時的一個關(guān)鍵任務(wù)是進(jìn)行一致性測試。即判斷在變換后所得到的計算機(jī)系統(tǒng)是否與模型表示相一致。,形式規(guī)約,形式規(guī)約(FormalSpecification,也稱形式規(guī)范或形式化描述)它是對程序“做什么”(

10、whattodo)的數(shù)學(xué)描述,是用具有精確語義的形式語言書寫的程序功能描述,它是設(shè)計和編制程序的出發(fā)點(diǎn),也是驗(yàn)證程序是否正確的依據(jù)。對形式規(guī)約通常要討論其一致性(自身無矛盾)和完備性(是否完全、無遺漏地刻畫所要描述的對象)等性質(zhì)。,形式規(guī)約,形式規(guī)約的方法主要可分為兩類:一類是面向模型的方法也稱為系統(tǒng)建模,該方法通過構(gòu)造系統(tǒng)的計算模型來刻畫系統(tǒng)的不同行為特征；另一類是面向性質(zhì)的方法也稱為性質(zhì)描述,該方法通過定義系統(tǒng)必須滿足的一些性質(zhì)來描述一個系統(tǒng)。,形式規(guī)約,不同的形式規(guī)約方法要求不同的形式規(guī)約語言,即用于書寫形式規(guī)約的語言(也稱形式化描述語言),代數(shù)語言O(shè)BJ、Clear、ASL、ACTOn

11、e/Two等進(jìn)程代數(shù)語言CSP、CCS、演算等；時序邏輯語言PLTL、CTL、XYZ/E、UNITY、TLA等；這些規(guī)約語言由于基于不同的數(shù)學(xué)理論及規(guī)約方法，因而也千差萬別，但它們有一個共同的特點(diǎn),即每種規(guī)約語言均由基本成分和構(gòu)造成分兩部分構(gòu)成。前者用來描述基本(原子)規(guī)約,后者把基本部分組合成大規(guī)約。構(gòu)造成分是形式規(guī)約研究和設(shè)計的重點(diǎn)，也是衡量規(guī)約語言優(yōu)劣的主要依據(jù)。,一個簡化的生命周期模型,定義軟件需求文檔SRD在完成需求搜集和分析之后，得到了軟件需求文檔SRD。它可被當(dāng)作客戶與軟件提供者之間的合同。定義軟件需求規(guī)格或行為規(guī)格(BS)軟件需求規(guī)格（或行為規(guī)格）在不去考慮系統(tǒng)的具體實(shí)現(xiàn)方法的

12、前提下，描述了系統(tǒng)所期望的是什么。它以SRD中所聲明的對象為基礎(chǔ)，根據(jù)從外部可觀察到的系統(tǒng)功能特征，來對所期望的系統(tǒng)行為進(jìn)行準(zhǔn)確和明確的描述。如果存在對系統(tǒng)的約束，也可將其作為系統(tǒng)的特征來進(jìn)行說明。,一個簡化的生命周期模型,定義設(shè)計規(guī)格(DS)設(shè)計規(guī)格在保持需求規(guī)格所聲明的特征的前提下，指明系統(tǒng)的運(yùn)行特點(diǎn)和內(nèi)部結(jié)構(gòu)。并可能根據(jù)一些具體需要，提供實(shí)現(xiàn)其行為的機(jī)制。設(shè)計規(guī)格與行為規(guī)格相比，增加了更多的細(xì)節(jié)。然而必須確保這些細(xì)節(jié)不改變需求規(guī)格所定義的系統(tǒng)的外部行為。通過增加越來越多的數(shù)據(jù)、行為、控制，以及異常描述等方面的細(xì)節(jié)，設(shè)計規(guī)格細(xì)化軟件需求規(guī)格，并對需求規(guī)格進(jìn)行更具體地描述。,一個簡化的生命周

13、期模型,對于設(shè)計規(guī)格中的每一個組件，可以更加詳細(xì)地指定組件的界面和組件間的交互，并進(jìn)一步細(xì)化成一系列的規(guī)格。從而得到界面規(guī)格和詳細(xì)設(shè)計規(guī)格或程序規(guī)格(PS)。詳細(xì)設(shè)計規(guī)格可以用程序來實(shí)現(xiàn)。,規(guī)格可以采用非形式化的方式描述，包括自然語言、圖、表等，也可以采用形式化方式描述。由于非形式化方法本身所存在的矛盾、二義性、含糊性，以及描述規(guī)格時的不完整性、抽象層次混雜等情況，使得所得到的規(guī)格不能準(zhǔn)確地刻畫系統(tǒng)模型，甚至?xí)楹髞淼能浖_發(fā)埋下出錯的隱患。,形式化方法由于基于嚴(yán)格的數(shù)學(xué)基礎(chǔ)，具有嚴(yán)格的語法和語義定義，從而可以準(zhǔn)確地描述系統(tǒng)模型，排除了矛盾、二義性、含糊性等情況。在對系統(tǒng)進(jìn)行嚴(yán)格地描述的過程中

14、，將會幫助開發(fā)人員和用戶明確那些原本模糊的需求，并發(fā)現(xiàn)用戶所陳述的需求中存在的矛盾，有利于相對完整、正確地理解用戶需求，最終得到一個完整、正確的系統(tǒng)模型。,形式化規(guī)格精確地描述了用戶的需求、軟件系統(tǒng)的功能以及各種性質(zhì)，其描述的是“做什么”，而不考慮“怎么做”。在書寫規(guī)格時應(yīng)該注意的一個問題是：如何描述得恰如其分，既不過多也不過少。在規(guī)格中描述過多會導(dǎo)致“實(shí)現(xiàn)偏向”，給實(shí)現(xiàn)施加了不必要的限制，從而排除了一些原本是合理的實(shí)現(xiàn)。描述得過少又有容納不合理實(shí)現(xiàn)的危險。為了開發(fā)出良好的規(guī)格，除了應(yīng)透徹理解、熟練掌握所使用的形式規(guī)格語言和方法外，還應(yīng)對所要描述的系統(tǒng)有全面深入的了解。,已建立了多種適用于軟件

15、系統(tǒng)規(guī)格的形式化方法，可分為三類：操作類描述類雙重類操作類方法基于狀態(tài)和轉(zhuǎn)移，通過可執(zhí)行模型來描述系統(tǒng)，模型本身能夠采用靜態(tài)分析和模型執(zhí)行而得到驗(yàn)證，這類方法包括有限狀態(tài)機(jī)、Statecharts、Petri網(wǎng)等。,描述類方法基于數(shù)學(xué)公理和概念，通過邏輯或代數(shù)給出系統(tǒng)的狀態(tài)空間，具有高度抽象的特點(diǎn)，便于通過自動工具進(jìn)行驗(yàn)證?；诓煌臄?shù)學(xué)基礎(chǔ)，描述類方法進(jìn)一步分為：基于代數(shù)的描述類方法，如Z、VDM、Larch等。基于邏輯的描述類方法，如命題線性時態(tài)邏輯(PropositionalLinearTemporalLogic，PLTL)一階線性時態(tài)邏輯(FirstOrderLinearTernpor

16、alLogic，PLTL)計算樹邏輯(ComputationTreeTemporalLogic，CTTL)等時態(tài)邏輯為代表,雙重類方法則兼有前面二者的特點(diǎn)，既能夠通過數(shù)學(xué)公理和概念來高度抽象地描述系統(tǒng)，又具有狀態(tài)和轉(zhuǎn)移的可執(zhí)行特征。這類方法包括：擴(kuò)展?fàn)顟B(tài)機(jī)實(shí)時時態(tài)邏輯(ExtendedStateMachineReal一TimeTemporalLogic，ESMRTTL)TRIO+TROL等,20世紀(jì)80年代，牛津大學(xué)和Hursley實(shí)驗(yàn)室合作將Z方法，用于開發(fā)IBM商用信息控制系統(tǒng)。IBM對整個開發(fā)所進(jìn)行的測試表明：明顯地改善了產(chǎn)品質(zhì)量大量地減少了錯誤和早期診斷錯誤其總體開發(fā)成本降低了9（IB

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

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

19、保密系統(tǒng)：NATO控制指揮和控制系統(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)運(yùn)輸系統(tǒng)：巴黎地鐵的自動火車保護(hù)系統(tǒng)、英國鐵路信號控制、以色列機(jī)載航空電子軟件。,形式化驗(yàn)證,軟件開發(fā)中的絕大部分錯誤是在需求分析和規(guī)格的早期階段引入的，這些錯誤將隨著開發(fā)的深入而逐漸放大。并且，這些錯誤發(fā)現(xiàn)得越晚，對其修改所需付出的代價也將會越大。在傳統(tǒng)的軟件開發(fā)方法中，除了在各個開發(fā)階段進(jìn)行評審以發(fā)現(xiàn)錯誤外，更多的錯誤則是直到編碼結(jié)束后的測試階段才能被檢測出。形式化方法在開發(fā)出形式規(guī)格后就進(jìn)行形式

20、驗(yàn)證。實(shí)際上是使得驗(yàn)證工作得以提前進(jìn)行，既可以提前發(fā)現(xiàn)錯誤，同時在修改所發(fā)現(xiàn)的錯誤時需要付出的代價也是最小的。,形式化驗(yàn)證,形式化驗(yàn)證的主要技術(shù)包括模型檢驗(yàn)和定理證明模型檢驗(yàn)是一種基于有限狀態(tài)模型并檢驗(yàn)該模型的期望特性的技術(shù)。模型檢驗(yàn)就是對模型的狀態(tài)空間進(jìn)行蠻力搜索，以確認(rèn)該系統(tǒng)模型是否具有某些性質(zhì)。搜索的可終止性依賴于模型的有限性。模型檢驗(yàn)主要適用于有窮狀態(tài)系統(tǒng)。,形式化驗(yàn)證,模型檢驗(yàn)的優(yōu)點(diǎn)完全自動化并且驗(yàn)證速度快當(dāng)所檢驗(yàn)的性質(zhì)未被滿足時，將終止搜索過程并給出反例。這種信息常常反映了系統(tǒng)設(shè)計中的失誤，因而對于用戶排錯有極大的幫助。模型檢驗(yàn)可用于系統(tǒng)的部分規(guī)格，即對于只給出了部分規(guī)格的系統(tǒng)，通

21、過搜索也可以提供關(guān)于已知部分正確性的有用信息。,形式化驗(yàn)證,模型檢驗(yàn)方法的一個嚴(yán)重缺陷是“狀態(tài)爆炸問題”。即，隨著所要檢驗(yàn)的系統(tǒng)的規(guī)模增大，模型檢驗(yàn)算法所需的時間空間開銷往往呈指數(shù)增長，因而極大地限制了其實(shí)際使用范圍。有序二叉決策圖(OrderedBinaryDecisionDiagrams，OBDD)是表述狀態(tài)轉(zhuǎn)移系統(tǒng)的高效率方法，使得較大規(guī)模系統(tǒng)的驗(yàn)證成為可能。模型檢驗(yàn)可以處理100至200個狀態(tài)變量的系統(tǒng)。模型檢驗(yàn)已用來檢驗(yàn)狀態(tài)數(shù)目可達(dá)10120的系統(tǒng)。并且通過采用適當(dāng)?shù)某橄蠹夹g(shù)，就可以處理具有更多狀態(tài)的系統(tǒng)。,形式化驗(yàn)證,模型檢驗(yàn)離不開模型檢驗(yàn)工具的支持。已有的模型檢驗(yàn)工具可分為時態(tài)邏

22、輯模型檢驗(yàn)工具行為一致檢驗(yàn)工具復(fù)合檢驗(yàn)工具。時態(tài)邏輯模型檢驗(yàn)工具有EMC、CESAR、SMV、Murphi、SPIN、UV、SVE、HyTech、Kronos等行為一致檢驗(yàn)工具有CospanFormalllCheck、FDR等；復(fù)合檢驗(yàn)工具有HSIS、VIS、STeP、METAFrame等。,形式化驗(yàn)證,貝爾實(shí)驗(yàn)室在FormalCheck下，對其高級數(shù)據(jù)鏈路控制器進(jìn)行了模型檢驗(yàn)，以驗(yàn)證功能。他們對6個性能進(jìn)行了規(guī)格，其中5個驗(yàn)證無誤，另外一個失敗，從而進(jìn)一步發(fā)現(xiàn)了一個影響信道流量的Bug。樓宇抗震分布式主動結(jié)構(gòu)控制系統(tǒng)的設(shè)計規(guī)格的系統(tǒng)模型有2.121019數(shù)目的狀態(tài)。經(jīng)過模型檢驗(yàn)，自動分析并發(fā)

23、現(xiàn)了影響主動控制效果的計時器設(shè)置錯誤。,形式化驗(yàn)證,基于SMV輸入語言建立了IEEEFuturebus+896.1一1991標(biāo)準(zhǔn)下cache一致協(xié)議的精確模型，通過SMV驗(yàn)證了轉(zhuǎn)移系統(tǒng)模型滿足cache一致性的規(guī)格。從中發(fā)現(xiàn)了先前并未找到和潛在的協(xié)議設(shè)計中的錯誤。Murphi有限狀態(tài)模型檢驗(yàn)工具對IEEE標(biāo)準(zhǔn)1596一1992下cache一致協(xié)議進(jìn)行了驗(yàn)證，發(fā)現(xiàn)了變量、邏輯等方面的錯誤。,形式化驗(yàn)證,Philips公司音響設(shè)備的控制協(xié)議通過HyTech得到了完全自動驗(yàn)證，這是一個具有離散和連續(xù)特征的混雜系統(tǒng)的驗(yàn)證問題。對AT&T公司的7500條通信軟件的SDL源代碼進(jìn)行了驗(yàn)證，從中發(fā)現(xiàn)112個

24、錯誤，約55的初始設(shè)計需求在邏輯上不一致。,形式化驗(yàn)證定理證明,定理證明采用邏輯公式來規(guī)格系統(tǒng)及其性質(zhì)。邏輯公式由一個具有公理和推理規(guī)則的形式化系統(tǒng)給出。進(jìn)行定理證明的過程就是應(yīng)用這些公理或推理規(guī)則來證明系統(tǒng)具有某些性質(zhì)。不同于模型檢驗(yàn)，定理證明可以處理無限狀態(tài)空間問題。,形式化驗(yàn)證定理證明,定理證明系統(tǒng)可分為自動和交互式兩種類型。自動定理證明系統(tǒng)是通用搜索過程，在解決各種組合問題中比較成功。交互式定理證明系統(tǒng)需要與用戶進(jìn)行交互，要求用戶能提供驗(yàn)證中創(chuàng)造性最強(qiáng)部分(建立斷言等)的工作，因而其效率較低，較難用于大系統(tǒng)的驗(yàn)證。,形式化驗(yàn)證定理證明,定理證明的的實(shí)施同樣需要定理證明器的支持?，F(xiàn)有的定

25、理證明器包括：用戶導(dǎo)引自動推演工具證明檢驗(yàn)器復(fù)合證明器,形式化驗(yàn)證定理證明,用戶導(dǎo)引自動推演工具有ACL2、Eves、LP、Nqthm、Reve和RRI這些工具由引理或者定義序列導(dǎo)引，每一個定理采用已建立的推演和引理，進(jìn)行自動證明。證明檢驗(yàn)器有Coq、HOL、LEGO、LCF和Nuprl復(fù)合證明器Analytica中將定理證明和符號代數(shù)系統(tǒng)Mathematica復(fù)合，PVS和Step將決策過程、模型檢驗(yàn)和交互式證明復(fù)合在一體。,形式化驗(yàn)證定理證明,基于符號代數(shù)運(yùn)算的自動定理證明用于證明Pentium中SRT算法的正確性，檢查出了一個錯誤。ACL2用于AMD5K86的浮點(diǎn)除微代碼的規(guī)格和機(jī)械證明

26、，ACL2還用來檢驗(yàn)浮點(diǎn)方根微的代碼的正確性，發(fā)現(xiàn)了其中的Bug，并對修改后的微代碼進(jìn)行了正確性的機(jī)器證明。ACL2用于Motorola復(fù)數(shù)算術(shù)處理器CSP的完全規(guī)格，同時對CSP的幾個算法進(jìn)行了驗(yàn)證。PVS用于航空電子微處理器AAMP5的規(guī)格和驗(yàn)證，對209條AAMP5指令中的108條進(jìn)行了規(guī)格，驗(yàn)證了11個有代表性的微代碼。,程序求精,程序求精又稱為程序變換，是將自動推理和形式化方法相結(jié)合而形成的一門技術(shù)。它研究從抽象的形式規(guī)格推演出具體的面向計算機(jī)的程序代碼的全過程。程序求精的基本思想是用一個抽象程度低、過程性強(qiáng)的程序去代替一個抽象程度高、過程性弱的程序，并保持它們之問功能的一致性。這里

27、所說的“程序”與傳統(tǒng)觀點(diǎn)中“可以由計算機(jī)直接執(zhí)行”的“程序”不同，這里的“程序”是對規(guī)格、設(shè)計文檔，以及程序代碼的統(tǒng)稱。,程序求精,因此，“程序”可以劃分為若干層次最高層是不能直接執(zhí)行的程序，即規(guī)格，它由抽象的描述語句構(gòu)成。最低層是可以直接執(zhí)行的程序，稱為程序代碼，它由可執(zhí)行的命令語句構(gòu)成。最高層和最低層之間為一系列混合程序，其中既含有抽象的描述語句，又含有可執(zhí)行的命令語句。,程序求精,程序開發(fā)過程實(shí)際上就是從最高層的程序開始，通過一系列的求精變換步驟，每一步都降低一些抽象程度或增加一些可執(zhí)行性，最終得到能夠指導(dǎo)計算機(jī)明確執(zhí)行的程序代碼。在進(jìn)行求精的過程中要注意保證程序的正確性，即保證所得到的

28、程序是滿足最初的形式規(guī)格的。程序的這種正確性可以通過求精過程中所遵循的一系列規(guī)則來保證，也可以在事后采用驗(yàn)證工具來證明。,程序求精,程序求精技術(shù)是形式化方法研究的一個熱點(diǎn)。在已出現(xiàn)的許多相關(guān)技術(shù)中，真正能夠應(yīng)用到實(shí)際軟件開發(fā)過程中的并不多。目前比較典型的是IBMHursley公司和牛津大學(xué)PRG程序設(shè)計研究組提出的針對Z規(guī)格的求精方法，以及CarrollMogan的規(guī)則求精方案。,程序求精,形式化開發(fā)方法一直受到多方面的爭議，這些爭議主要體現(xiàn)在：形式化方法中所包含的數(shù)學(xué)理論，限制了大多數(shù)程序設(shè)計人員的學(xué)習(xí)和使用。采用形式化方法會延誤項(xiàng)目開發(fā)周期，增加開發(fā)費(fèi)用。許多流行的形式化方法對于較小規(guī)模項(xiàng)

29、目是有效的，但卻很難應(yīng)用于大型項(xiàng)目。形式化方法不能確保開發(fā)出完全正確的軟件缺乏對軟件生命周期內(nèi)各個階段提供全面支持的形式化方法等。,程序求精,形式化方法中的抽象數(shù)學(xué)符號及理論確實(shí)給軟件工程師的使用帶來一些不便，以致于人們要花時間和精力去學(xué)習(xí)和掌握。但是，采用形式化方法可以極大地減少系統(tǒng)設(shè)計開發(fā)早期階段的錯誤，避免后期錯誤修改所帶來的高額成本開銷。采用形式化方法還會提高系統(tǒng)的開發(fā)效率。并且形式化方法是高質(zhì)量、高可靠性軟件開發(fā)的有效途徑，是軟件自動化的根本前提。,程序求精,形式化方法不會完全代替非形式化的軟件開發(fā)方法，軟件工程師們需要根據(jù)所解決問題的特點(diǎn)結(jié)合或選擇使用。,程序求精,形式化方法結(jié)合到

30、具體的軟件開發(fā)過程中需要考慮如下一些因素：應(yīng)用的類型：形式化方法不可能對所有的應(yīng)用類型都適用。對于一個項(xiàng)目，應(yīng)該衡量其問題領(lǐng)域的特點(diǎn)以及模型的復(fù)雜性，從而確定是否適于采用形式化方法。,程序求精,規(guī)模和結(jié)構(gòu)：在將形式化方法用于一個項(xiàng)目之前，還應(yīng)該評價項(xiàng)目的規(guī)模和結(jié)構(gòu)復(fù)雜性。形式化方法可有效地適用于中等規(guī)模的系統(tǒng)。為了使大型系統(tǒng)能充分受益于所采用的形式化方法，該系統(tǒng)應(yīng)該具有很好的結(jié)構(gòu)，并能分解成定義良好的構(gòu)件，從而使其中的關(guān)鍵部分只受形式化方法的控制。類型的選擇：在將形式化方法用于一個項(xiàng)目時，必須能清楚地確定其目標(biāo)。不同的應(yīng)用目的將對開發(fā)過程產(chǎn)生不同的影響，從而影響到對形式化方法類型的選擇。,程序

31、求精,形式化級別：對一個系統(tǒng)可能進(jìn)行非形式化、半形式化或者高度形式化的描述。從某個給定項(xiàng)目的目標(biāo)出發(fā)，必須先確定其應(yīng)用的關(guān)鍵程度、項(xiàng)目規(guī)模、可用的資源，以及對項(xiàng)目合適的形式化程度等，并從這些可能性中做出一個選擇。使用范圍：雖然形式化方法可使用于開發(fā)過程的所有階段，但通常只是有選擇地使用。一方面需要對形式化方法所應(yīng)用于的開發(fā)階段進(jìn)行選擇，另一方面，需要對采用形式化方法的構(gòu)件進(jìn)行選擇。對那些決定安全性的構(gòu)件不但需要形式化，而且需要高度的形式化。,程序求精,工具：為了足夠精確地實(shí)施形式化方法，工具的支持是必須的。,程序求精,形式化方法在軟件產(chǎn)業(yè)中應(yīng)用的深入有賴于諸多方面工作的進(jìn)展。需要開發(fā)出將整體特性分解為易于驗(yàn)證的局部特性的有效方法大規(guī)模復(fù)雜軟件中搜索空間是巨大的，需要研究新的處理方法形式化方法與非形式化方法的結(jié)合形式化方法和新的軟件開發(fā)技術(shù)（如SOA）的結(jié)合需要有效的軟件工具,程序求精,具有良好用戶界面、容易學(xué)習(xí)和