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