形式化描述是使用形式化語言來詳細描述軟體需求和特性的一種方法，它解決了軟體「做什麼」的問題。這種方法可以分為兩類：
建立計算模型來描述系統的行為特性。
定義系統必須滿足的屬性來描述系統。
形式化描述，也稱為形式化規約，與自然語言描述相比，具有以下特點：
精確性：避免了模糊性和二義性。
可驗證性：可以通過形式化驗證來檢查系統是否滿足其描述。
消除矛盾：在需求定義中消除相互矛盾的地方。
減少理解偏差：避免需求定義人員和開發人員對需求的理解偏差。
形式化描述是形式化方法的重要組成部分，它與形式化驗證一起，為軟體開發提供了一個更加嚴謹和可靠的基礎。