系列簡介：形式化方法在計算機和軟件工程學科中作為一個學科分支，正在越來越多地進入工業界諸多實踐領域。以DO-333適航標準為代表的工業標準，亦對軟件開發過程明確提出了采用形式化方法的要求。為此，結合上海控安形式化方法技術團隊歷年來在航空、航天和軌交等領域的成功應用經驗，本專題將圍繞“形式化方法”特別是形式化方法的工程化應用，組織一系列文章，探討形式化方法背后的動因和關鍵技術及行業應用。

01

傳統軟件工程面臨的困難

自從1968年“軟件工程”這個學科概念提出以來，軟件工程的研究和實踐有效地解決了軟件的質量和研制效率問題。但是傳統軟件工程中存在的大量依賴人工的活動和主觀性判斷等過程和技術，給軟件帶來了日趨明顯的可信問題。我們以工業領域最常見的 “V”字模型為例探討傳統軟件工程中的一些局限性。

圖1 常見于工業標準的V字模型

按照V模型的軟件開發過程，我們可以看到，即使是工業界較為推崇的V模型，其描述的軟件研制過程仍然存在明顯的局限性和風險：

（1）軟件研制過程中文檔的準確性

軟件需求普遍以自然語言來撰寫需求文檔。由于自然語言天然的二義性和模糊性，造成文檔難以精確描述軟件預期功能和性能。設計文檔采用圖形化描述，往往缺乏嚴格的語法和語義。此類中間產物的缺陷往往持續傳遞至代碼和測試階段，部分深層次問題幾乎始終無法探測。

（2）軟件研制過程對主觀活動的依賴性

軟件研制過程中，各階段的轉換及產物之間的一致性，嚴重依賴人工判斷。例如設計文檔是否與需求文檔中功能和行為描述一致，往往通過人工審查和比對來進行。

（3）軟件研制過程的嚴謹性

軟件研制過程中的中間產物，缺乏嚴格分析手段。例如，自然語言撰寫的需求文檔難以被嚴格分析。設計文檔刻畫的系統架構，通過簡單的仿真進行而缺少對系統行為深層次的驗證，例如死鎖等安全隱患難以揭示。

盡管業界和學術界在軟件工程理論和實踐中取得了豐碩成果，軟件質量問題始終是行業的一大難題。2017年11月28日 俄羅斯“聯盟-2.1B”火箭發射失敗，軟件錯誤導致19顆衛星燒毀。波音737MAX機型的控制軟件對人機控制優先級的錯誤設計，導致2018年和2019年兩次惡性墜機事件。

隨著軟件產品對社會生產生活的重要性日趨上升，如何改善并發展現有的軟件工程方法，使其能對軟件的安全可信提供更為可靠的保障，成為了工業界和學術界普遍關心的問題。在此背景下，形式化方法以其嚴謹的數學理論基礎和不斷發展的技術手段，被視為一種極有潛力的解決方案。

02

形式化方法發展歷史

在20世紀60年代，Floyd、Hoare和Manna等試圖用數學方法來證明程序的正確性并發展成了各種程序驗證方法。隨后軟件工程界認識到了數學方法的巨大潛力，形式化方法一詞開始傳播開來。1969-1972年之間， C.A.R Hoare撰寫了"計算機編程的公理基礎"和"數據表示的正確性證明"兩篇開創性的論文，并提出了規格說明的概念。

在形式語義與形式化建模以及形式化規約的基礎上，將計算機系統的分析與驗證問題轉化為邏輯推理問題或者形式模型的判斷問題，用定理證明工具/求解器或者某個形式模型的原型工具來進行驗證。交互式定理證明需要用戶與計算機相互協助來進行形式化證明。最常用的證明輔助是Coq和Isabelle，均有在空客等航空領域項目中成功應用的記錄。

模型檢驗的基本思想是通過遍歷系統的狀態空間以驗證系統模型是否滿足給定的關鍵性質，并在不滿足性質時給出具體反例路徑。例如在航空等安全攸關領域，常用于分析系統是否滿足給定的功能需求或安全性質。較有代表性的工具包括SPIN、UPPAAL和 PRISM等，在工業界尤其是在硬件系統的分析與驗證上取得了很大的成功。

關于形式化驗證的定理證明、模型檢測等方法，特別是在軌交、航空、航天和汽車電子及工業控制等行業的成功應用以及相關工具的研發，我們將在后續的文章中作更為深入和系統化的探討。

03

形式化方法的簡介

形式化方法(Formal Methods)是一種基于數學的開發軟件系統的方法學，它提供了一種數學化的框架，在此框架之下開發者可以通過定義系統和驗證系統的方式，以系統化的手段逐步開發軟件。

從廣義上講，形式化方法是指將離散數學的方法用于解決軟件工程領域的問題，主要包括建立精確的數學模型以及對模型的分析活動。狹義地講，形式化方法是運用形式化語言，進行形式化的規格描述、模型推理和驗證的方法。

通常來說，形式化方法強調了對軟件預期功能和行為的“描述（specify）”和“驗證（verify）”。描述強調通過精確的形式化語言刻畫軟件，驗證則強調通過數學手段嚴格地分析軟件是否是一致的、是否滿足給定的性質等。由此我們可以認為，形式化方法包含兩項目主要分支，形式化規格說明技術和形式化驗證技術。這兩種技術都是基于數學基礎，例如集合論、邏輯和代數理論等，如圖3所示。

圖3 形式方法的構成

形式化規格說明技術可以視為一種對軟件形式化建模的過程。一般來說，形式化建模需要有特定的形式化語言，此類語言基本上可以分為下述類型：

基于模型的語言

此類形式化語言基本思想是利用一些已知特性的數學抽象來為目標軟件系統的狀態特征和行為特征構造模型，包括域、元組、集合等。Z、VDM，B等都是面向模型的語言。

代數方法語言

代數方法僅使用帶有等詞的一階邏輯的表示，而不引入通常的數學對象。常見的代數方法有Larch等。

進程代數語言

進程代數提供了描述并發系統所需的并行復合，選擇，順序復合等語句。并可通過等式推理（equatioanl reasoning）的方法來驗證系統滿足某些性質。常見的進程代數語言有CSP等。

形式化驗證就是基于已建立的形式化規格說明的基礎上，對所描述系統的相關性質進行分析以評判系統是否滿足期望的性質，盡可能地發現其中的不一致性、模糊性、不完備性等錯誤。形式化驗證的主要技術包括定理和模型檢測。

定理證明技術是形式方法的核心，定理證明系統是由一個形式語言和推理機制構成的形式系統。推理機制由公理和推理規則組成。通常的定理證明過程需要工具的支持。使用定理證明技術，我們可以對用戶期望的或系統應具有的性質進行證明，以消除規格說明中的模糊性、不一致性、不安全性等。

模型檢測是一種自動驗證系統正確性的方法。模型檢測器的輸入通常是一個系統的有限狀態模型以及一組用時態邏輯表達的系統預期的性質。通過搜索有限狀態模型所有的可能事件序列來判定系統性質是否得到滿足。由于系統的模型是有限的，因此系統狀態空間的搜索能終止。假如系統的性質成立，則模型檢測器輸出一個肯定結果。如果性質不滿足，則系統輸出一個以狀態序列表示的反例。

一個最簡單的例子：

假如在一個飛行器中有一款控制軟件，需要完成飛行控制行為。其中某條功能為“求一個給定正數的非負數平方根”。我們用形式化語言Z來描述這條軟件功能，如圖4所示。

圖4 模式SquareRootSpec

其中的E形框稱為模式框架 (Schema Box)，可以近似看作一個“操作”，頂部的標識符 SquareRootSpec 稱為模式名稱，中間水平線起分隔作用，水平線上部稱為聲明部分，水平線下面是謂詞部分，由若干個謂詞組成，這些謂詞通過聯結詞“∧”形成一個完整的謂詞。該例中將radicand? 和squareroot! 都聲明為實數類型，分別為輸入變量和輸出變量。

從這個例子可以看出，形式化語言刻畫軟件功能時，更多地是通過一種數學上的“抽象”來精確描述待開發的軟件。在這個例子里，求平方根的細節過程并不是重點要刻畫的對象，而是通過“squareroot!2= radicand?”這個等式來表達一種“關系”，即“待求的非負數平方根，其平方一定等于被開方數”。對于軟件來說，這種關系是必然的、唯一的，而代碼實現求解的方式則是多樣的。

上面這個例子里，若我們把Z語言撰寫的模式看作是一個“軟件需求的形式化描述”，那么我們就可以對這個形式化的需求做進一步的分析驗證。假定，我們想表達的是“求一個給定正數的非負數平方根”，但是寫需求的人員，誤將要輸出的非負數平方根變量squareroot!寫成了負數平方根，即整個謂詞部分變成了“radicand?≥0 ∧ squareroot! 2= radicand? ∧squareroot!<0”。此時我們該如何發現這個缺陷呢？

假定需求分析過程中，我們還有一位需求檢查者。檢查者可以通過數學證明的方式來發現這個缺陷。例如，檢查者可以在謂詞表達式之后插入一個斷言“squareroot! ≥0”。此時，謂詞表達式應該滿足這個斷言。

通過數學證明的方式，顯然可以發現，“radicand?≥0 ∧ squareroot! 2= radicand? ∧squareroot!<0”是無法推出“squareroot! ≥0”的，即原先撰寫的謂詞與給定的斷言相矛盾。

上面的例子是一個非常簡單的示例，僅用于說明最簡單的形式化描述和分析過程。在我們后續的推文中，我們將陸續深入闡釋形式化建模和形式化驗證的相關技術以及其行業應用。

審核編輯：符乾江