什麼是形式化驗證？

什麼是形式化驗證？

Peter 王廣忠

程序員，專業區塊鏈講解員

編者按：本文由Peter 王廣忠的技術分享，轉載請註明來自Peter 王廣忠，並聯系作者獲得授權。Peter 王廣忠，程序員，專業區塊鏈講解員

Peter 最近的文章中很多都是針對一個具體的技術點的，核心論述思路是，某某某是什麼，為何它很重要。今天的這篇也不例外，瞄準的技術點叫做 Formal Verification ，形式化驗證。

什麼是形式化驗證？

形式化驗證是用數學方法去證明我們的系統是無 Bug 的。

首要的一步是用數學語言描述清楚我們要解決的問題。通過對問題建立數學模型，限定系統在不同時刻應該有的狀態，以及不應該有的狀態。然後用這些數學規則去限定系統的設計以及實現。

傳統上在硬件設計領域比較常用。主要原因就是硬件設計週期長，成本高，一旦生產出來就很難改動了。例如一個 CPU 設計如果已經出芯片了，那麼出了問題就是大事。Peter 自己以前所在的能源動力領域，很多電廠設備也都要做數學上的論證，不過我們那會兒不用形式化驗證這個詞，我們叫建模，或者叫軟件模擬。如果直接用一臺機器去做各種試驗，那麼成本是很高的，而用數學去構建一臺虛擬的機器去驗證，既可以運行全部的輸入和輸出，做到論證充分，同時又沒有太高的成本。

總之，形式化驗證就是用數學去精確的論證一個系統，可以是硬件系統，但是本文要重點聊的是它在軟件開發領域的崛起。

為何大部分程序員都沒聽說過？

但是大部分的程序員可能從來都沒用過形式化驗證，這是為啥呢？

首先就是因為軟件迭代太快了。尤其在互聯網領域，創新是不變的主題，對一套系統建立數學模型是有很高的時間成本的，對於要頻繁迭代的系統就顯得不適合了。

軟件很容易升級。跟硬件不一樣，軟件有了 Bug ，可以連夜修復，很多用戶根本不會注意到。萬一有用戶遇到了 bug ，起碼後臺數據庫的數據一般不會損壞，打個電話，讓客服幫忙弄一下，誰家的軟件又沒 bug 呢？

軟件是有測試的。對於沒有寫過代碼的同學可能不太熟悉什麼叫做寫測試。寫測試，也就是去寫一些能有驗證代碼的代碼。測試代碼中其實往往也會模擬一些輸入和輸出情況的。形式化驗證是超豪華版的測試，用嚴格的數學論證，保證邏輯沒有死角。

總之，軟件的形式化驗證其實多年來一直也有人搞研究，但是在產業界不是很常見。

為何形式化驗證對程序員變得越來越重要？

軟件的形式化驗證最近的火爆，最直接的觸發因素是區塊鏈技術的崛起，但是在整個軟件開發行業，也都有這個趨勢。

如果事關生死，高成本也值了。比如我們要寫控制火車調度的軟件，或者寫控制醫療設備的嵌入式軟件，那麼僅僅寫幾行測試代碼，或者交給黑盒測試團隊，去覆蓋百分之九十九的可能，這是遠遠不夠的。我們需要不計成本的去提高軟件的可靠性，這時候形式化驗證就很有必要了。對於區塊鏈領域，代碼即法律，代碼控制著我們的數字身份，控制著我們的智能合約中的資金，這些情況下，如果出了問題，可不是給客服打電話就能解決的，區塊鏈行業中很多人經歷過 The DAO 事件，一小段時間內，大家眼睜睜看著黑客不斷的把大家智能合約中的錢轉走，教訓很慘痛。

所以在軟件開發領域，形式化驗證也變得越來越受到重視。

總結

關於形式化驗證的一個簡單的介紹，內容就是這些了。要記住的重點是，形式化驗證是用數學方法去保證系統無 Bug 的方法，特點是成本很高，所以傳統上只是在硬件領域比較流行，但是隨著軟件正在人們生活中扮演越來越重要的角色，形式化驗證也逐漸被很多程序員所重視。