形式化驗證方法淺析

陳波 李夫明

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

關鍵詞：形式化驗證方法;軟件設計;硬件驗證;模型檢測;定理證明

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

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

1 概述

硬件和軟件系統在規模和功能上的增長增加了復雜性，也增加了潛在錯誤的可能性，這些錯誤引起了金錢、時間上的損失，甚至會危及人們的生命。形式方法是用于軟件和硬件系統的規范，開發和驗證的特定類型的基于數學的技術，是改善和確保系統質量的重要方法。形式化方法在軟件和硬件領域中的應用進展比較顯著，引起了各個領域的注意[1]。形式化驗證方法是形式化方法的一個重要的研究內容，本文主要對形式化驗證方法進行探討。

2 基本概念

2.1 形式化規范說明

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

不同的形式規范說明方式要求不同的形式化規范語言。下面是用于順序和并發系統形式規范的常見方法及語言：

2.2 形式化驗證

形式驗證是使用正式的數學方法證明或反駁系統相對于某個正式規范或屬性的預期算法的正確性的行為，形式驗證要求產品的規范和實現均需要有嚴格的形式描述[2]，如圖2所示。主要有兩種方法，一類是以邏輯推理為基礎，邏輯推理有se-quent calculus， resolution natural deduction，以及Hoare-logic等方法，統稱為定理證明技術;另一類則以窮盡搜索為基礎統稱為模型檢測。

2.2.1 定理證明

定理證明：先對系統及其性質進行抽取，表示成基于某種邏輯的命題、謂詞、定理，在驗證者的引導下，不斷地對公理、以證明的定理施加推理規則，產生新的定理，直到推導出表達系統性質的公式，從而證明設計的系統滿足該性質。現在定理證明器越來越多的應用在驗證硬件和軟件設計的安全臨界性質的驗證[3]。

定理證明高度抽象，具有強大的邏輯表達能力，可以驗證幾乎所有的系統行為特性，可以處理無限的狀態空間。定理證明器可以分為三種：自動定理證明器、交互式定理證明器及證明檢驗器。現在大多數定理證明器是交互式的，需要人的引導，對驗證者的要求有良好的數學經驗。

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

2.2.2 模型檢測

模型檢測是建立一個系統的有限狀態模型并檢測希望滿足的性質在這個模型中是否成立的技術。

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

自動化程度較高是模型檢測的優點，并且當系統不滿足給定的性質時，可以給出反例，使設計人員方便找出設計錯誤。模型檢測應用于硬件和協議的驗證，現在在對軟件設計的驗證已成為研究的熱點。狀態空間爆炸問題是其主要的缺點。

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

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

3 形式化驗證方法的優缺點

3.1 形式化驗證方法的優點

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

3.2 形式化驗證方法的不足

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

4 形式化驗證方法發展的展望

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

4.1 基本概念

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

4.2 方法和工具

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

5 結束語

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

參考文獻：

[1]韓俊剛，杜慧敏.數字硬件的形式化驗證[M].北京大學出版社，北京：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]張廣泉.形式化方法導論[M].清華大學出版社，北京：2015.12.

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

【通聯編輯：王力】

收稿日期：2019-08-21

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