形式化方法與軟件開發

什麼是形式化方法

用於開發計算機系統的形式化方法是基於數學的用於描述系統性質的技術。這樣的形式化方法提供了一個框架，人們可以在該框架中以系統的方式刻畫，開發和驗證系統。也就是，在軟件開發的全過程中，凡是採用嚴格的數學語言，具有精確的數學語義的方法，都稱為形式化方法。

廣義角度，是軟硬件開發過程中分析，設計及做到的系統工程方法，狹義角度，是軟硬件規格和驗證的方法

軟件形式化方法開發的過程

首先模型獲取：

從現實世界向模型表示轉換的過程，包括如何提取模型，如何表示模型。對應軟件的需求分析，規格以及設計

其次模型驗證：

對所得到的模型進行檢驗，判斷其是否捕獲了所有的用戶需求，以及該模型是否具有所期望的特性。

最後模型變換：

從模型表示向計算機系統變換的過程，一個抽象的模型表示可以變換到各種計算機環境上，主要的任務是進行一致性測試，判斷在變換過程中所得到的計算機系統是否與模型表示一致。

形式化方法在軟件開發中的優缺點

優點：

1.將非形式化的需求轉換成形式化規約的過程中，二義性、需求的增量和矛盾較易發現

2.形式模型將導致層次化的半自動甚至是自動化的系統開發方法

3.與通常的用例測試相比，形式化方法可以用數學的方法驗證其正確性

4.一個經過驗證的子系統可以並入一個形式或非形式的大的系統中，這將增加系統符合規約的可信度

5.使得開發者可以評估、比較各種不同的設計

缺點：

1.包含數學理論，限制大多數設計人員學習

2.使用形式化方法會增加開發所用時間和費用

3.不能確保開發完全正確的軟件

4.很難應用1於一些大型系統

5.缺乏對軟件生命周期各個階段提供全面支持的形式化方法