作者 |馮勁草上海控安可信軟件創(chuàng)新研究院研究員

版塊 |鑒源論壇 · 觀模

01形式化方法基本概念

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.1 定理證明技術(shù)

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

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

3.1.1簡單推理舉例

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

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

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

3.1.2定理證明舉例

同上述章節(jié)中推導(dǎo)出來的數(shù)學(xué)運(yùn)算的性質(zhì)等同，在程序中，使用Hoare logic來證明程序的部分正確性。它以一階邏輯為基礎(chǔ)，利用運(yùn)算規(guī)則、公理與推理規(guī)則進(jìn)行程序證明。即：如果斷言P在程序S執(zhí)行前為真時(shí)可推出斷言R在S終止時(shí)為真，則程序S對(duì)于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}成立，則對(duì)于所有Q=>P，{Q} S {R}均成立。根據(jù)上述兩條公理，當(dāng)我們想證一條{P}S{R}成立時(shí)，我們可以根據(jù)賦值公理找到一個(gè)一定使后置條件滿足的情況{R[f/x]}x:=f{R},當(dāng)P能夠=>P[f/x]時(shí)，{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模型檢測(cè)技術(shù)

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

3.2.1 模型檢測(cè)舉例

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

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

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

關(guān)于形式化驗(yàn)證的定理證明、模型檢測(cè)等方法在行業(yè)中的實(shí)際應(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.

審核編輯黃宇