作者 |馮勁草上?？匕部尚跑浖?chuàng)新研究院研究員

版塊 |鑒源論壇 · 觀模

01形式化方法基本概念

形式化方法是基于嚴(yán)格的數(shù)學(xué)基礎(chǔ)，通過采用數(shù)學(xué)邏輯證明來對計算機軟硬件系統(tǒng)進(jìn)行建模、規(guī)約、分析、推理和驗證，是用于保證計算機軟硬件系統(tǒng)正確性以及安全性的一種重要方法。

形式化方法使用數(shù)學(xué)及邏輯證明的手段對計算機系統(tǒng)進(jìn)行建模、規(guī)約、分析、推理，其主要涵蓋以下幾個研究方向：定理證明、形式模型、形式語義與形式建模、形式規(guī)約、形式驗證技術(shù)。下面以高可信工業(yè)領(lǐng)域?qū)嶋H應(yīng)用中最廣泛的形式化規(guī)格說明、定理證明和模型檢測為例，介紹其基本原理。

02形式化規(guī)格說明

通過對編程語言的語義進(jìn)行嚴(yán)格的定義，加之使用形式模型對計算機系統(tǒng)的行為進(jìn)行建模，最終形成形式化規(guī)格說明書來對計算機系統(tǒng)的行為進(jìn)行推理驗證，形式規(guī)格說明是對計算機系統(tǒng)進(jìn)行驗證的基礎(chǔ)，形式規(guī)格說明的基礎(chǔ)是形式語義學(xué)和形式建模。

形式語義學(xué)（formal semantic）是研究程序設(shè)計語言的語義的學(xué)科，以數(shù)學(xué)為工具，利用符號和公式，精確地定義和嚴(yán)格地解釋計算機程序設(shè)計語言的語義，從而消除設(shè)計者、開發(fā)者和使用者之間的理解的差異性。形式語義幫助理解語言，指導(dǎo)語言的設(shè)計，幫助編寫編譯器和語言系統(tǒng)，支持程序驗證和軟件可靠性，有助于軟件規(guī)范化。形式語義學(xué)主要分為四大流派：操作語義，代數(shù)語義，指稱語義和公理語義。操作語義著重模擬數(shù)據(jù)處理過程中程序的操作；代數(shù)語義基于代數(shù)，用代數(shù)結(jié)構(gòu)刻畫程序語法實體，用代數(shù)公理刻畫實體含義以及語法實體間的關(guān)系；指稱語義主要刻畫數(shù)據(jù)處理的結(jié)果，而不是處理的細(xì)節(jié)；公理語義用公理化的方式描述程序?qū)?shù)據(jù)的處理，主要用于程序的推理和論證。早期的程序語言的語義只是在論文中給出，不能用計算機測試語義的正確性和一致性，也不能用于程序的驗證和分析。中期的語義一般用定理證明器的元語言實現(xiàn)，此類語義可用于程序語言語義和程序性質(zhì)的手動或半自動驗證。K框架是最近流行的定義語言的形式語義的途徑，基于重寫邏輯，通過定義語言的操作語義，自動生成對應(yīng)程序的形式分析和驗證工具。

形式建模是對計算機軟硬件系統(tǒng)的行為和性質(zhì)用某種形式模型精確的刻畫。形式模型一般采用通用形式建模語言（如Petri Net、Event-B、Pi-演算、CSP、SysML、Lusture等）或者專用形式模型（如有限自動機、下推自動機、概率自動機等）來進(jìn)行。函數(shù)式程序可以用樹自動機、高階下推自動機來建模，自適應(yīng)系統(tǒng)與多智能體一般使用Petri網(wǎng)、UML、Z以及馬爾可夫模型等來建模，對于深度神經(jīng)網(wǎng)絡(luò)的形式建模最近也成為研究熱點。

2.1 形式化規(guī)格說明舉例

假設(shè)有一個“農(nóng)夫過河”系統(tǒng)，其需求文檔如下：

（1）一個人帶著狼、山羊和白菜在一條河的左岸，有一條船，大小正好能裝下這個人和其它三者之一，人和他的隨行物都要帶過岸，但他每次只能帶一樣?xùn)|西擺渡過河。

（2）如人將狼和羊留在同一岸，無人照顧，那么狼會把羊吃掉。同樣，如羊和白菜在同一岸，無人照顧，那么羊會吃了白菜。

該系統(tǒng)在設(shè)計完成后，應(yīng)當(dāng)滿足性質(zhì)：至少存在一條過河路徑，使得人和他的隨行物全部渡過了河。

為了驗證上述系統(tǒng)是否滿足相對應(yīng)的性質(zhì)，使用NuSMV形式化驗證工具進(jìn)行性質(zhì)的驗證工作。NuSMV是一款經(jīng)典的基于BDDs(Binary Decision Diagrams)的模型驗證器。在本例中，我們將使用NuSMV提供的形式化描述語言對一個系統(tǒng)的需求進(jìn)行形式化規(guī)格說明的轉(zhuǎn)化。

用對上述自然語言描述的需求文檔進(jìn)行形式化建模，使用NuSMV的形式化語言描述如圖1所示。

圖1 農(nóng)夫過河系統(tǒng)的形式化規(guī)格說明

對待驗證的性質(zhì)使用性質(zhì)描述語言進(jìn)行描述，如圖2所示。

圖2 待驗證性質(zhì)的形式化描述

使用NuSMV進(jìn)行模型檢測的基本原理是將形式化語言描述的系統(tǒng)和待驗證的性質(zhì)抽取形成一個狀態(tài)遷移系統(tǒng)，在該狀態(tài)遷移系統(tǒng)中若存在一個可接收狀態(tài)即為該系統(tǒng)滿足特定性質(zhì)。后續(xù)的形式化驗證工作即是建立在該形式化規(guī)格說明上的。

03形式化驗證技術(shù)

3.1 定理證明技術(shù)

在形式語義與形式建模以及形式規(guī)約的基礎(chǔ)上，將計算機系統(tǒng)的分析與驗證問題轉(zhuǎn)化為邏輯推理問題或者形式模型的判斷問題，用定理證明工具/求解器或者某個形式模型的原型工具來進(jìn)行驗證。形式化驗證主要的技術(shù)有定理證明和模型檢測。

定理證明的基本思想是，將程序滿足其形式規(guī)約的證明問題轉(zhuǎn)化為一組數(shù)學(xué)命題的證明。若這一組數(shù)學(xué)命題，稱作證明義務(wù)（proof obligation），能夠蘊含“程序滿足其規(guī)約”這一命題，那么我們可以說該證明系統(tǒng)是正確（sound）的。

3.1.1簡單推理舉例

在數(shù)學(xué)運算中，有許多運算公理及其推導(dǎo)出的運算屬性。在給出如圖3所示的運算公理時，證明運算屬性P1：x=x+y*0 成立便是一個簡單的推理證明過程。推理證明過程如圖4所示。

圖3數(shù)學(xué)運算公理

圖4 數(shù)學(xué)運算屬性證明過程

3.1.2定理證明舉例

同上述章節(jié)中推導(dǎo)出來的數(shù)學(xué)運算的性質(zhì)等同，在程序中，使用Hoare logic來證明程序的部分正確性。它以一階邏輯為基礎(chǔ)，利用運算規(guī)則、公理與推理規(guī)則進(jìn)行程序證明。即：如果斷言P在程序S執(zhí)行前為真時可推出斷言R在S終止時為真，則程序S對于P和R來說是正確的，使用三元組表示為：{P} S {R}。

嘗試證明：{x <> y∧x > y} x := y – 1 {x = y ∨ x < y}的正確性。在該語句中，P={x<>y ∧x > y} ；S=x:=y-1；Q={x = y ∨ x < y}。為了證明該語句，需要使用兩條公理，一條是賦值公理（Ass-D0），一條是推論規(guī)則。賦值公理指，{P[f/x]} x := f {P}成立，P[f/x]是用f替代P中所有x得到的謂詞表達(dá)式。推論規(guī)則指：如果{P} S {R}成立，則對于所有Q=>P，{Q} S {R}均成立。根據(jù)上述兩條公理，當(dāng)我們想證一條{P}S{R}成立時，我們可以根據(jù)賦值公理找到一個一定使后置條件滿足的情況{R[f/x]}x:=f{R},當(dāng)P能夠=>P[f/x]時，{P}S{R}得證。如圖5所示，使用賦值公理，將后置條件中的x使用賦值語句中的x=y-1替代，得到{y y∧x >y}=>{y y∧x > y} x := y – 1 {x = y ∨ x < y}成立。由于y < y + 1 <=> true,所以{ x <> y∧x >y}=>{y y∧x > y} x := y – 1 {x = y ∨ x < y}成立。

圖5 賦值公理的使用過程

3.2模型檢測技術(shù)

模型檢驗的基本思想是通過遍歷系統(tǒng)的狀態(tài)空間以驗證系統(tǒng)模型是否滿足給定的關(guān)鍵性質(zhì)，并在不滿足性質(zhì)時給出具體反例路徑。因此，如何對模型狀態(tài)空間進(jìn)行快速遍歷對于模型檢驗至關(guān)重要，而狀態(tài)空間爆炸問題則自然成為模型檢驗技術(shù)面臨的主要問題。與模型檢驗技術(shù)取得成功的硬件領(lǐng)域相對比，軟件系統(tǒng)的狀態(tài)空間復(fù)雜性更高。將相關(guān)狀態(tài)空間符號化表達(dá), 并在符號化后的空間上進(jìn)行計算和遍歷是軟件模型檢驗的基本方法。然而，即使是符號化后的狀態(tài)空間，其驗證也并不是一個簡單問題，因此對復(fù)雜的狀態(tài)空間進(jìn)行抽象簡化是一個重要研究方向。

3.2.1 模型檢測舉例

將上述章節(jié)中的農(nóng)夫過河系統(tǒng)轉(zhuǎn)化成相應(yīng)的狀態(tài)遷移圖如圖6所示，其中MGCW-Empty表示初始狀態(tài)，“-”左邊的符號表示對應(yīng)的符號在左岸?！?”右邊的服務(wù)表述對應(yīng)的符號在右岸。M表示人，G表示羊，C表示白菜，W表示狼，箭頭表示表示每次在船上運輸?shù)奈锲返姆N類。其中因為有一些約束限制所以導(dǎo)致一些理論上會出現(xiàn)的狀態(tài)并沒有出現(xiàn)。

圖6 農(nóng)夫過河狀態(tài)遷移圖

該系統(tǒng)待驗證的性質(zhì)在該圖中可表述為初始狀態(tài)為“MGCW-Empty”的情況下， 是否存在一條路徑，能夠到達(dá)終止?fàn)顟B(tài)“Empty-MGCW”。即在圖6中，是否存在一條路徑，使得狀態(tài)1能夠到達(dá)狀態(tài)8。若存在該路徑，那么說明經(jīng)過驗證，該系統(tǒng)滿足了該性質(zhì)，若不存在該路徑，那么說明經(jīng)過驗證，該系統(tǒng)不滿足該性質(zhì)。

關(guān)于形式化驗證的定理證明、模型檢測等方法在行業(yè)中的實際應(yīng)用情況，我們將在后續(xù)的章節(jié)中陸續(xù)為大家介紹。

主要參考文獻(xiàn)：

1. Jifeng He: A New Roadmap for Linking Theories of Programming. UTP 2016: 26-43.

2. CCF Formal Methods Technical Committee. Advances and trends on formal methods. In: The Progress Report of Computer Science and Technology in China from 2017 to 2018. Beijing: China Machine Press, 2018. 1-68(in Chinese with English abstract).

3. Ro?u G, ?erb?nut? T F. An overview of the K semantic framework[J]. The Journal of Logic and Algebraic Programming, 2010, 79(6): 397-434.

4. Cimatti A , Clarke E , Giunchiglia F . NUSMV: a new symbolic model checker[J]. International Journal on Software Tools for Technology Transfer, 2000, 2(4):410-425.

5. Wang S, Zhan N, Zou L. An improved HHL prover: an interactive theorem prover for hybrid systems[C]//International Conference on Formal Engineering Methods. Springer, Cham, 2015: 382-399.

6. Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[C]//Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 1977: 238-252.

審核編輯黃宇