#版權宣告
主要針對希賽出版的架構師考試教程《系統架構設計師教程（第4版）》，作者“希賽教育軟考學院”。完成相關的讀書筆記以便後期自查，僅供個人學習使用，不得用於任何商業用途。

文章目錄

• 第七節 形式化方法

第七節 形式化方法

形式化方法是指採用嚴格的數學方法，使用形式化規約語言來精確定義軟體系統。非形式化的開發方法是通過自然語言、圖形或表格描述軟體系統的行為和特性，然後基於這些描述進行設計和開發，而形式化開發則是基於數學的方式描述、開發和驗證系統。

形式化方法包括形式化描述和基於形式化描述的形式化驗證兩部分內容。

• 形式化描述又稱之為形式化規約，就是用形式化語言進行描繪，建立軟體需求和特性，即解決軟體“做什麼”的問題。形式化描述，相對於自然語言描述，形式化描述是精確的、可驗證的，避免了模糊性與二義性，消除需求中相互矛盾的地方，避免需求定義人員和開發人員對需求的理解偏差。
  • 通過建立計算模型來描述系統的行為特性
  • 通過定義系統必須滿足的一些屬性來描述系統
• 形式化驗證指的是驗證已有的程式是否滿足形式化描述的定義。

形式化描述可以通過計算機技術進行自動處理，進行一致性的檢查和證明，提高需求分析的效率和質量。通過形式化描述，需求分析的質量大大提高，很多自然語言描述無法避免的缺陷在需求分析階段就會被發現，並得到解決，從而降低後期開發和維護的成本，並提升軟體的質量和可靠性。

在一些要求高可靠性的關鍵應用上，採用形式化開發方法可以保證軟體系統的可靠性。如巴黎地鐵 14 號線和 Roissy 機場穿梭車的自動控制系統。這兩個系統中的部分程式使用了形式化方法進行開發，並取得了很好的效果，如表 6-1 所示。

表 6-1 中的 ADA 程式碼行數表示運用形式化方法開發的軟體系統規模，這些程式碼是形式化方法自動生成的，開發人員並不需要直接修改這些程式碼。