形式化模型
所属分类
是软工开发模型中的一种，也可以称为形式化方法模型，与之相关的有形式验证。关于软件开发模型，可以参考这里软件开发模型。
概念
形式化模型的主要活动是生成计算机软件形式化的数学规格说明。形式化方法使软件开发人员可以应用严格的数学符号来说明、开发和验证基于计算机的系统。形式化方法的本质是基于数学的方法来描述目标软件系统属性的一种技术。
形式化方法原则上就是用数学与逻辑的方法描述和验证软件。从描述上讲，一方面是系统或程序的描述，另一方面是性质的描述。这些可以用一种或多种语言来描述。这些语言包括命题逻辑，一阶逻辑，高阶逻辑，代数，状态机，并发状态机，自动机，计算树逻辑，线性时序逻辑，进程代数， π-演算， μ-演算，特殊的程序语言，以及程序语言的子集等。从验证来讲，主要有两类方法，一类是以逻辑推理为基础，另一类则以穷尽搜索为基础。逻辑推理有 natural deduction, sequent calculus, resolution 以及Hoare-logic 等方法，穷尽搜索方法统称为模型检测。这类方法与系统或程序以及系统性质的表示有很大的关系，比如说符号模型检测，其基本原理是用命题逻辑公式表示状态转换关系，用不动点算法计算状态的可达性以及这些状态是否满足某些性质。
形式化方法需要形式化规约说明语言的支持。
特点
开发者通过使用一个严格的数学符号体系来描述、开发和验证基于计算机的系统。
使用形式化方法能够更容易发现和纠正二义性、不完整性和不一致性等其他软件过程模型难以克服的问题。它不是依靠特定的评审，而是应用数学分析的方法。在设计阶段，形式化方法是程序验证的基础，使软件开发人员能够发现和改正一些往往被忽略的问题。
局限性
开发很费时、昂贵。
具备所必须背景的开发者太少。
对于技术水平不高的客户，很难用这种模型进行沟通。
存在原因
尽管有这些疑虑，软件开发者中还是有很多形式化方法的追随者，比如有人用其开发高度关注安全性的软件（如飞行器和医疗设施），或者开发出错将导致重大经济损失的软件。虽然不是一种主流的方法，形式化方法的意义在于可以提供无缺陷的软件。应用场景有下：
安全性、可靠性至关重要时
软件发生错误会导致严重经济损失时
总结
以上只是要点，要想深入了解，请移步软件形式化方法概述(强烈推荐，总结很好)。
实例
推荐书籍
古天龙.软件开发的形式化方法.高等教育出版社