形式化方法(Formal Methods)，在邏輯科學中是指分析、研究思維形式結構的方法。它把各種具有不同內容的思維形式(主要是命題和推理)加以比較，找出其中各個部分相互聯結的方式,如命題中包含概念彼此間的聯結，推理中則是各個命題之間的聯結，抽取出它們共同的形式結構；再引入表達形式結構的符號語言，用符號與符號之間的聯絡表達命題或推理的形式結構。

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

由上圖可知，形式化方法還包含了：

形式化驗證、形式語言等內容。

形式化驗證：

在計算機硬體（特別是積體電路）和軟體系統的設計過程中，形式驗證的含義是根據某個或某些形式規範或屬性，使用數學的方法證明其正確性或非正確性。

在計算機硬體（特別是積體電路）和軟體系統的設計過程中，形式化驗證的含義是根據某個或某些形式化規範或屬性，使用數學的方法證明其正確性或非正確性。

形式語言：

在數學、邏輯和電腦科學中，形式語言（英語：Formal Language）是用精確的數學或機器可處理的公式定義的語言。

如語言學中語言一樣，形式語言一般有兩個方面：語法和語義。專門研究語言的語法的數學和電腦科學分支叫做形式語言理論，它只研究語言的語法而不致力於它的語義。在形式語言理論中，形式語言是一個字母表上的某些有限長字串的集合。一個形式語言可以包含無限多個字串。

?

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

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