#yyds干货盘点# 可信软件的形式化建模与方法

形式化模型来源于原始需求的逐步演化求精，因此不可避免地存在各种各样的错误，例如语法错误、功能缺失，功能之间存在逻辑上的不一致等。为了保证形式化模型能完整无缺且正确地描述人们对软件的真实期望，需要有一定的方法对形式化模型进行分析与验证。

形式化系统分析与验证分为以下几个步骤:

（1）通过数据流描述、变量关系描述和软件体系结构描述等图形符号，从形式化需求模型中抽取不同形态的分析模型。

（2）根据软件的特点划分为不同分析目标，为每个验证分析目标定义出相应技术。

（3）针对建立的性质集合，采用模型检测的方法自动地发现漏dong与验证软件是否满足高安全可靠性需求。

（4）自动生成测试用例，基于系统模型及需求自动生成关于软件实现的测试用例集，提高系统测试的效率和错误发现能力。

（5）将形式化模型进行仿真。仿真主要用于检测模型中人们所关心的系统行为在执行时是否存在错误，是一种类似于“运行”系统来暴露错误和缺陷的分析方法。

相对于测试，形式化验证的方法就是借助数学的思想和方法对软件程序是否满足性质归约进行证明或者证伪。因其高度严谨的特点，形式化验证成为保障软件正确性的关键方法。目前最主流的形式化验证技术有如下两种：