文章目录
[+]
什么是形式化方法
用于开发计算机系统的形式化方法是基于数学的用于描述系统性质的技术。这样的形式化方法提供了一个框架，人们可以在该框架中以系统的方式刻画，开发和验证系统。也就是，在软件开发的全过程中，凡是采用严格的数学语言，具有精确的数学语义的方法，都称为形式化方法。
广义角度，是软硬件开发过程中分析，设计及实现的系统工程方法，狭义角度，是软硬件规格和验证的方法
（图片来自网络侵删）
软件形式化方法开发的过程
首先模型获取：
从现实世界向模型表示转换的过程，包括如何提取模型，如何表示模型。对应软件的需求分析，规格以及设计
其次模型验证：
对所得到的模型进行检验，判断其是否捕获了所有的用户需求，以及该模型是否具有所期望的特性。
最后模型变换：
从模型表示向计算机系统变换的过程，一个抽象的模型表示可以变换到各种计算机环境上，主要的任务是进行一致性测试，判断在变换过程中所得到的计算机系统是否与模型表示一致。
形式化方法在软件开发中的优缺点
优点：
1.将非形式化的需求转换成形式化规约的过程中，二义性、需求的增量和矛盾较易发现
2.形式模型将导致层次化的半自动甚至是自动化的系统开发方法
3.与通常的用例测试相比，形式化方法可以用数学的方法验证其正确性
4.一个经过验证的子系统可以并入一个形式或非形式的大的系统中，这将增加系统符合规约的可信度
5.使得开发者可以评估、比较各种不同的设计
缺点：
1.包含数学理论，限制大多数设计人员学习
2.使用形式化方法会增加开发所用时间和费用
3.不能确保开发完全正确的软件
4.很难应用1于一些大型系统
5.缺乏对软件生命周期各个阶段提供全面支持的形式化方法
