從廣義上講，形式化方法（Formal Method）是指将離散數學的方法用于解決軟體工程領域的問題，主要包括建立精确的數學模型以及對模型的分析活動。狹義的講，形式化方法是運用形式化語言，進行形式化的規格描述、模型推理和驗證的方法。将形式化方法運用于軟體工程實踐當中的主要目的是保證軟體的正确性。
軟體開發實際上就是把現實世界的需求映射成軟體的模型化過程。在進行模型化的過程中涉及到三種系統模型：現實世界、模型表示和計算機系統。軟體形式化過程即使在這三類系統之間進行描述和轉化的過程。開發過程中的任務依次包括：模型擷取、模型驗證、模型變換。
軟體規格說明是對軟體系統對象，對象的操作方法，以及對象行為的描述。非形式化的規格說明可用自然語言、圖、表等形式來描述。形式證明與驗證技術主要包括模型檢測和定理證明。程式求精是将自動推理和形式化方法相結合，從抽象的形式規約推演出具體的面向計算機的程式代碼的全過程。
模态（Modal）邏輯是經典命題邏輯和一階謂詞邏輯的擴充形式。一階線性時态邏輯（FOLTL）是一階謂詞邏輯的擴充。類似于PLTL，FOLTL 是在一階謂詞邏輯中增加了模态詞：必然、可能、下一時刻、直到。
計算機邏輯（CTL）是一種離散、分支時間、命題時态邏輯。在CTL中，除了具有時态算子必然，可能，下一時刻，直到外，還增加了路徑量詞：所有未來路徑(A)、至少某一路徑（E）。軟體的計算機樹邏輯規格可以通過模型檢驗得到驗證。模型檢驗就是在軟體系統的Kripke結構模型下，對以CTL*公式給出的軟體性質的正确性驗證。