軟體形式化方法

軟體形式化方法是指建立在嚴格數學基礎上的軟體開發方法。形式化方法模型的主要活動是生成計算機軟體形式化的數學規格說明。形式化方法使軟體開發人員可以套用嚴格的數學符號來說明、開發和驗證基於計算機的系統。

起源

軟體形式化方法最早可追溯到20世紀50年代後期對於程式設計語言編譯技術的研究，即J.Backus提出BNF描述Algol60語言的語法，出現了各 種語法分析程式自動生成器以及語法制導的編譯方法，使得編譯系統的開發從“手工藝製作方式”發展成具有牢固理論基礎的系統方法。

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

內容

形式化方法的本質是基於數學的方法來描述目標軟體系統屬性的一種技術。不同的形式化方法的數學基礎是不同的，有的以集合論和一階謂詞演算為基礎（如Z和VDM），有的則以時態邏輯為基礎。形式化方法需要形式化規約說明語言的支持。

這樣的形式化方法提供了一個框架，可以在框架中以系統的而不是特別的方式刻劃、開發和驗證系統。如果一個方法有良好的數學基礎，那么它就是形式化的，典型地以形式化規約語言給出。這個基礎提供一系列精確定義的概念，如：一致性和完整性，以及定義規範的實現和正確性。形式化方法模型的主要活動是生成計算機軟體形式化的數學規格說明。形式化方法使軟體開發人員可以套用嚴格的數學符號來說明、開發和驗證基於計算機的系統。這種方法的一個變型是淨室軟體工程（cleanroom software engineering），這一軟體工程方法目前已套用於一些軟體開發機構。

分類

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

1. 面向模型的形式化方法。面向模型的方法通過構造一個數學模型來說明系統的行為。
   
2. 面向屬性的形式化方法。面向屬性的方法通過描述目標軟體系統的各種屬性來間接定義系統行為。
   

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圖，狀態圖等。