从广义上讲，形式化方法（Formal Method）是指将离散数学的方法用于解决软件工程领域的问题，主要包括建立精确的数学模型以及对模型的分析活动。狭义的讲，形式化方法是运用形式化语言，进行形式化的规格描述、模型推理和验证的方法。将形式化方法运用于软件工程实践当中的主要目的是保证软件的正确性。
软件开发实际上就是把现实世界的需求映射成软件的模型化过程。在进行模型化的过程中涉及到三种系统模型：现实世界、模型表示和计算机系统。软件形式化过程即使在这三类系统之间进行描述和转化的过程。开发过程中的任务依次包括：模型获取、模型验证、模型变换。
软件规格说明是对软件系统对象，对象的操作方法，以及对象行为的描述。非形式化的规格说明可用自然语言、图、表等形式来描述。形式证明与验证技术主要包括模型检测和定理证明。程序求精是将自动推理和形式化方法相结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。
模态（Modal）逻辑是经典命题逻辑和一阶谓词逻辑的扩展形式。一阶线性时态逻辑（FOLTL）是一阶谓词逻辑的扩展。类似于PLTL，FOLTL 是在一阶谓词逻辑中增加了模态词：必然、可能、下一时刻、直到。
计算机逻辑（CTL）是一种离散、分支时间、命题时态逻辑。在CTL中，除了具有时态算子必然，可能，下一时刻，直到外，还增加了路径量词：所有未来路径(A)、至少某一路径（E）。软件的计算机树逻辑规格可以通过模型检验得到验证。模型检验就是在软件系统的Kripke结构模型下，对以CTL*公式给出的软件性质的正确性验证。