形式化方法

在計算機科學和軟體工程領域，形式化方法是基於數學的特種技術，適合於軟體和硬體系統的描述、開發和驗證。將形式化方法用於軟體和硬體設計，是期望能夠像其它工程學科一樣，使用適當的數學分析以提高設計的可靠性和魯棒性。但是，由於採用形式化方法的成本高意味著它們通常只用於開發注重安全性的高度整合的系統。

形式化方法在古代就運用了，而在現代邏輯中又有了進一步的發展和完善。這種方法特別在數學、計算機科學、人工智慧等領域得到廣泛運用。它能精確地揭示各種邏輯規律，制定相應的邏輯規則，使各種理論體系更加嚴密。同時也能正確地訓練思維、提高思維的抽象能力。

軟體形式化方法最早可追溯到20世紀50年代後期對於程序設計語言編譯技術的研究，即J.Backus提出BNF描述Algol60語言的語法，出現了各 種語法分析程序自動生成器以及語法制導的編譯方法，使得編譯系統的開發從“手工藝製作方式”發展成具有牢固理論基礎的系統方法。形式化方法的研究高潮始於 20世紀60年代後期，針對當時所謂“軟體危機”,人們提出種種解決方法，歸納起來有兩類：一是採用工程方法來組織、管理軟體的開發過程；二是深入探討程 序和程序開發過程的規律，建立嚴密的理論，以其用來指導軟體開發實踐。前者導致“軟體工程”的出現和發展，後者則推動了形式化方法的深入研究。經過30多 年的研究和應用，如今人們在形式化方法這一領域取得了大量、重要的成果，從早期最簡單的形式化方法——一階謂詞演算方法到現在的應用於不同領域、不同階段 的基於邏輯、狀態機、網路、進程代數、代數等眾多形式化方法。形式化方法的發展趨勢逐漸融入軟體開發過程的各個階段，從需求分析、功能描述(規約)、(體 繫結構/演演算法)設計、編程、測試直至維護。

用於開發計算機系統的形式化方法是描述系統性質的基於數學的技術，這樣的形式化方法提供了一個框架，可以在框架中以系統的而不是特別的方式刻劃、開發和驗 證系統。如果一個方法有良好的數學基礎，那麼它就是形式化的，典型地以形式化規約語言給出。這個基礎提供一系列精確定義的概念，如：一致性和完整性，以及定義規範 的實現和正確性。形式化方法的本質是基於數學的方法來描述目標軟體系統屬性的一種技術。不同的形式化方法的數學基礎是不同的，有的以集合論和一階謂詞演算為基礎（如Z和 VDM），有的則以時態邏輯為基礎。形式化方法需要形式化規約說明語言的支持。

形式化方法的一個重要研究內容是形式規約(Formal Specification,也稱形式規範或形式化描述),它是對程序“做什麼”(what to do)的數學描述，是用具有精確語義的形式語言書寫的程序功能描述，它是設計和編製程序的出發點，也是驗證程序是否正確的依據。對形式規約通常要討論其一 致性(自身無矛盾)和完備性(是否完全、無遺漏地刻畫所要描述的對象)等性質。形式規約的方法主要可分為兩類：一類是面向模型的方法也稱為系統建模，該方 法通過構造系統的計算模型來刻畫系統的不同行為特徵；另一類是面向性質的方法也稱為性質描述，該方法通過定義系統必須滿足的一些性質來描述一個系統。不同 的形式規約方法要求不同的形式規約語言，即用於書寫形式規約的語言(也稱形式化描述語言),如代數語言OBJ、Clear、ASL、ACT One/Two等；進程代數語言CSP、CCS、π演算等；時序邏輯語言PLTL、CTL、XYZ/E、UNITY、TLA等；這些規約語言由於基於不同 的數學理論及規約方法，因而也千差萬別，但它們有一個共同的特點，即每種規約語言均由基本成分和構造成分兩部分構成。前者用來描述基本(原子)規約，後者 把基本部分組合成大規約。構造成分是形式規約研究和設計的重點，也是衡量規約語言優劣的主要依據。

形式驗證形式化方法的另一重要研究內容是形式驗證(Formal Verification)。形式驗證與形式規約之間具有緊密的聯繫，形式驗證就是驗證已有的程序(系統)P，是否滿足其規約(φ,ψ)的要求(即P (φ,ψ)),它也是形式化方法所要解決的核心問題。傳統的驗證方法包括模擬(simulation)和測試(testing)，它們都是通過實驗的方法 對系統進行查錯。模擬和測試分別在系統抽象模型和實際系統上進行，一般的方法是在系統的某點給予輸入，觀察在另一點的輸出，這些方法花費很大，而且由於實 驗所能涵蓋的系統行為有限，很難找出所有潛在的錯誤。基於此，早期的形式驗證主要研究如何使用數學方法，嚴格證明一個程序的正確性(即程序驗證)。

根據說明目標軟體系統的方式，形式化方法可以分為兩類：

1）面向模型的形式化方法。面向模型的方法通過構造一個數學模型來說明系統的行為。

2）面向屬性的形式化方法。面向屬性的方法通過描述目標軟體系統的各種屬性來間接定義系統行為。

根據表達能力，形式化方法可以分為五類：

1）基於模型的方法：通過明確定義狀態和操作來建立一個系統模型（使系統從一個狀態轉換到另一個狀態）。用這種方法雖可以表示非功能性需求（諸如時間需求），但不能很好地表示併發性。如：Z語言，VDM，B方法等。

2）基於邏輯的方法：用邏輯描述系統預期的性能，包括底層規約、時序和可能性行為。採用與所選邏輯相關的公理系統證明系統具有預期的性能。用具體的編程構 造擴充邏輯從而得到一種廣譜形式化方法，通過保持正確性的細化步驟集來開發系統。如：ITL（區間時序邏輯），區段演算（DC），hoare 邏輯，WP演算，模態邏輯，時序邏輯，TAM（時序代理模型），RTTL（實時時序邏輯）等。

3）代數方法：通過將未定義狀態下不同的操作行為相聯繫，給出操作的顯式定義。與基於模型的方法相同的是，沒有給出併發的顯式表示。如：OBJ， Larch族代數規約語言等；

4）進程代數方法：通過限制所有容許的可觀察的過程間通信來表示系統行為。此類方法允許併發過程的顯式表示。如：通信順序過程（CSP），通信系統演算（CCS），通信過程代數（ACP），時序排序規約語言（LOTOS），計時CSP(TCSP），通信系統計時可能性演算（TPCCS）等。

5）基於網路的方法：由於圖形化表示法易於理解，而且非專業人員能夠使用，因此是一種通用的系統確定表示法。該方法採用具有形式語義的圖形語言，為系統開發和再工程帶來特殊的好處。如 Petri圖，計時Petri圖，狀態圖等。