陳波 李夫明

摘要：隨著信息技術(shù)的發(fā)展，軟硬件系統(tǒng)越來越復(fù)雜，其中軟硬件系統(tǒng)設(shè)計的正確性至關(guān)重要。形式化驗證方法在硬件設(shè)計和軟件開發(fā)等領(lǐng)域發(fā)揮越來越重要的作用，成為模擬驗證的重要補充。本文主要介紹了形式化驗證方法的發(fā)展現(xiàn)狀并對其發(fā)展進行展望。

關(guān)鍵詞：形式化驗證方法;軟件設(shè)計;硬件驗證;模型檢測;定理證明

中圖分類號：TP301 文獻標識碼：A

文章編號：1009-3044（2019）34-0239-02

1 概述

硬件和軟件系統(tǒng)在規(guī)模和功能上的增長增加了復(fù)雜性，也增加了潛在錯誤的可能性，這些錯誤引起了金錢、時間上的損失，甚至?xí)＜叭藗兊纳Ｐ问椒椒ㄊ怯糜谲浖陀布到y(tǒng)的規(guī)范，開發(fā)和驗證的特定類型的基于數(shù)學(xué)的技術(shù)，是改善和確保系統(tǒng)質(zhì)量的重要方法。形式化方法在軟件和硬件領(lǐng)域中的應(yīng)用進展比較顯著，引起了各個領(lǐng)域的注意[1]。形式化驗證方法是形式化方法的一個重要的研究內(nèi)容，本文主要對形式化驗證方法進行探討。

2 基本概念

2.1 形式化規(guī)范說明

形式化規(guī)范說明是明確的表達所要設(shè)計的系統(tǒng)的及其性質(zhì)的過程。形式化規(guī)范說明的語言具有嚴格的數(shù)學(xué)語法和語義，避免了自然語言的歧義性和不精確性[2]。可以用來表達系統(tǒng)的性質(zhì)：功能行為、時序行為、性能特征以及內(nèi)部結(jié)構(gòu)，力求達到無二義性、一致性和完整性。這些可以用一種或多種語言來描述。目前對行為性質(zhì)的形式化規(guī)范說明技術(shù)已經(jīng)很成熟。把不同的規(guī)范說明語言結(jié)合在一起對系統(tǒng)進行描述成為一種發(fā)展趨勢;另外一種趨勢是對系統(tǒng)的非行為方面：性能、實時限制、安全要求、結(jié)構(gòu)設(shè)計等進行形式化描述。

不同的形式規(guī)范說明方式要求不同的形式化規(guī)范語言。下面是用于順序和并發(fā)系統(tǒng)形式規(guī)范的常見方法及語言：

2.2 形式化驗證

形式驗證是使用正式的數(shù)學(xué)方法證明或反駁系統(tǒng)相對于某個正式規(guī)范或?qū)傩缘念A(yù)期算法的正確性的行為，形式驗證要求產(chǎn)品的規(guī)范和實現(xiàn)均需要有嚴格的形式描述[2]，如圖2所示。主要有兩種方法，一類是以邏輯推理為基礎(chǔ)，邏輯推理有se-quent calculus， resolution natural deduction，以及Hoare-logic等方法，統(tǒng)稱為定理證明技術(shù);另一類則以窮盡搜索為基礎(chǔ)統(tǒng)稱為模型檢測。

2.2.1 定理證明

定理證明：先對系統(tǒng)及其性質(zhì)進行抽取，表示成基于某種邏輯的命題、謂詞、定理，在驗證者的引導(dǎo)下，不斷地對公理、以證明的定理施加推理規(guī)則，產(chǎn)生新的定理，直到推導(dǎo)出表達系統(tǒng)性質(zhì)的公式，從而證明設(shè)計的系統(tǒng)滿足該性質(zhì)?，F(xiàn)在定理證明器越來越多的應(yīng)用在驗證硬件和軟件設(shè)計的安全臨界性質(zhì)的驗證[3]。

定理證明高度抽象，具有強大的邏輯表達能力，可以驗證幾乎所有的系統(tǒng)行為特性，可以處理無限的狀態(tài)空間。定理證明器可以分為三種：自動定理證明器、交互式定理證明器及證明檢驗器。現(xiàn)在大多數(shù)定理證明器是交互式的，需要人的引導(dǎo)，對驗證者的要求有良好的數(shù)學(xué)經(jīng)驗。

主要的定理證明工具有：STeP（Stanford）、TLV、AL2（UT Aus-tin/CLI）、Coq、HOL（Cambridge）、Isabelle（Cambridge）、Larch、Nu-prl、PVS（SRI）等。

2.2.2 模型檢測

模型檢測是建立一個系統(tǒng)的有限狀態(tài)模型并檢測希望滿足的性質(zhì)在這個模型中是否成立的技術(shù)。

目前有兩種主要模型檢測技術(shù)：一種是時態(tài)模型檢測，這種方法中規(guī)范說明用時態(tài)邏輯公式表示，系統(tǒng)用有限狀態(tài)轉(zhuǎn)換模型表示，用模型檢測器檢測模型是否滿足規(guī)范說明公式。另外一種是等價性檢測，這種方法中規(guī)范說明用一個自動機表示，系統(tǒng)用一個自動機表示，然后證明兩個模型是否一致。

自動化程度較高是模型檢測的優(yōu)點，并且當(dāng)系統(tǒng)不滿足給定的性質(zhì)時，可以給出反例，使設(shè)計人員方便找出設(shè)計錯誤。模型檢測應(yīng)用于硬件和協(xié)議的驗證，現(xiàn)在在對軟件設(shè)計的驗證已成為研究的熱點。狀態(tài)空間爆炸問題是其主要的缺點。

主要的模型檢測工具有：COSPAN/FORMAL CHECK（Bell）、MURPHY（Stanford）、SPIN（Bell）、SMV（CMU）、VIS（Berkeley）等。

目前形式化驗證方法成功應(yīng)用于商業(yè)、航空業(yè)、通信業(yè)和芯片制造業(yè)，INTEL，ARM和NIVIDA等大公司已經(jīng)把形式化方法應(yīng)用到芯片的制造和驗證[5]。

3 形式化驗證方法的優(yōu)缺點

3.1 形式化驗證方法的優(yōu)點

形式驗證是完備的，能夠完全斷定設(shè)計的正確性，對指定描述得所有可能情況進行驗證，不僅僅對其中的一個輸入子集進行多次試驗，克服了模擬實驗的不足[4]。形式驗證用數(shù)學(xué)方法將待驗證電路與功能描述直接進行比較，不需要開發(fā)測試用例。形式化驗證可以進行從系統(tǒng)級到門級的驗證驗證時間短，可以更早發(fā)現(xiàn)和改正設(shè)計缺陷，縮短周期和降低成本。形式驗證工具能夠自動驗證特性的正確性，極大地方便了測試者，減小驗證難度。形式驗證工具應(yīng)用斷言驗證的方法，斷言以注釋形式出現(xiàn)在代碼中，從而既不影響原有代碼的工作，又充分發(fā)揮了斷言驗證方法的作用，不影響原有驗證流程。

3.2 形式化驗證方法的不足

不管形式化驗證是軟件系統(tǒng)還是硬件設(shè)計，都要建立對象的各種模型，模型是在對原始設(shè)計進行抽象后所得到的，抽象出的模型和原始設(shè)計之間不可避免地存在鴻溝，而且驗證的完整性取決于特性是否被全面準確的表達。形式化驗證到目前為止仍然不能有效地的驗證電路的性能，如電路的延時和功耗等[4]。當(dāng)系統(tǒng)變復(fù)雜時，驗證將占用較多的計算機資源，耗時增加。如前文所述各種形式化驗證技術(shù)都有其固有的缺陷需要繼續(xù)研究克服。

4 形式化驗證方法發(fā)展的展望

形式化驗證方法的主要目的是幫助設(shè)計人員設(shè)計更可靠的系統(tǒng)。形式化驗證方法的進展依靠基礎(chǔ)理論研究、研制新的方法和工具、方法和工具的集成等。主要從概念、方法和工具以及和其他技術(shù)結(jié)合等方面提出幾點看法。

4.1 基本概念

形式化驗證方法在實際應(yīng)用中的顯著作用依賴于計算機科學(xué)各個領(lǐng)域的研究結(jié)果。以后的工作主要包括以下范圍：組織：必須對怎樣組織方法、規(guī)范說明、模型、定理、證明等有深刻理解;分解：開發(fā)一種更有效地把全局的性質(zhì)分解為更易驗證的子性質(zhì)的方法;抽象：不進行抽象很難對真實的系統(tǒng)進行規(guī)范和驗證，對不同的系統(tǒng)或問題域采用不同的抽象技術(shù);可復(fù)用模型和理論：對模型和理論進行復(fù)用可以減少工作量;數(shù)學(xué)理論的組合：很多安全臨界系統(tǒng)既有數(shù)字元件也有模擬元件，這樣的混合系統(tǒng)要求用離散和連續(xù)的數(shù)學(xué)理論進行推理;數(shù)據(jù)結(jié)構(gòu)和算法：對大的搜索空間和大的系統(tǒng)進行處理時，就要求開發(fā)新的數(shù)據(jù)結(jié)構(gòu)和算法。

4.2 方法和工具

為了吸引使用者，開發(fā)的工具和方法應(yīng)滿足以下特征：短的回收期、付出越多回報也越多、多用途、集成使用、易于使用、高效、易學(xué)、面向檢錯，聚焦分析、適應(yīng)系統(tǒng)的發(fā)展等。沒有任何一種方法或工具可以解決所有的問題，沒有一種形式化工具可以描述和分析復(fù)雜系統(tǒng)的任何一個方面，因此把各種方法和工具集成起來使用成為一種趨勢。主要是：模型檢測和定理證明技術(shù)的集成、形式化規(guī)范與驗證技術(shù)與傳統(tǒng)的開發(fā)過程的集成、軟件和硬件的設(shè)計驗證方法的集成等。在軟件工程中面向?qū)ο蠹夹g(shù)與形式方法相結(jié)合已經(jīng)成為一個比較熱的研究領(lǐng)域。形式化驗證方法在以太坊智能合約安全監(jiān)測中也得到廣發(fā)應(yīng)用。

5 結(jié)束語

本文主要探討了形式化驗證方法的有關(guān)基本概念，對形式化驗證方法的兩種主要形式：定理證明、模型檢測進行闡述，以及從使用角度分析了形式化驗證方法的優(yōu)缺點，最后提出了對形式化驗證方法的幾點見解。

參考文獻：

[1]韓俊剛，杜慧敏.數(shù)字硬件的形式化驗證[M].北京大學(xué)出版社，北京：2001.12.

[2] CLARKE E M， WING J M. Formal Methods：State of the Artand Future Directions[Jl.ACM Computing Surveys，1996，28（4）.

[3] Johann M.Schumann， Automated Theorem Proving in SoftwareEngineering，Spring-Verlag 2001.

[4]張廣泉.形式化方法導(dǎo)論[M].清華大學(xué)出版社，北京：2015.12.

[5]陳鋼，于林宇，裘宗燕，等.基于邏輯的形式化驗證方法：進展及應(yīng)用[J].北京大學(xué)學(xué)報：自然科學(xué)版，2016，52（2）.

【通聯(lián)編輯：王力】

收稿日期：2019-08-21

作者簡介：陳波（1981-），女，山東淄博人，碩士，山東理工大學(xué)計算機科學(xué)與技術(shù)學(xué)院，講師，研究方向為計算機軟件與理論。