形式化方法

是指建立在嚴格數學基礎上的系統開發 方法。它是保證設計正確性的一條重要的途徑。其中，邏輯、 代數、自動機、圖論等構成 了形 式化方法的數學基礎。形 式化方法的目的是希望所設計的系統具有較高的可信度和 正確性，並能使系統具有 良好的結構、易維護、能較好地滿 足使用者要求。實踐證明，通過形式規約確實可以增強對系統 發現其它方法難以發現的錯誤。越來越多的實踐證明，形式 化方法在系統設計和驗證，特別是高可靠性系統的設計和 驗證中有著不可取代的地位。經過 30多年的研究和應用， 如今，形式化方法這一領域取得了大量重要的成果，其應用 也是逐漸融入軟體開發過程的各個階段：從需求系統分析、 功能描述 、（體系結構/演算法)設計、程式設計、測試直至維護。

形式化方法主要包括形式化規約和形式化驗證技術。 形式規約是對系統需要達到的功能和性質的數學描述。它 是系統設計的出發點，也是驗證系統是否正確的依據，通過 形式化描述可 以儘早發現需求和設計中的錯誤 。

形式規約的方法主要可分為兩類 ：一類是對系統建模， 該方法的 目標是用合適的數學工具建立系統模型，藉此精 確地刻畫系統的行為特徵；另一類是性質描述 ，該方法的 目 標是用合適 的數學工具來描述系統的性質 ，藉此對系統進 行深入的研究。

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

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