C.5.12 形式化证明(验证)

注:在GB/T 20438.3--2017的表A.5与表A.9中引用了本技术/措施。

目的:使用了理论和数学模型及规则,证明程序针对其某种抽象模型的正确性。

描述:测试是一种检验程序正确性的常见方式。然而,实际值的程序的复杂性通常无法实现详尽的测试。因此只有一小部分可能的程序可以用这个方法检查。相反,形式化验证应用数学运算于一个程序的数学表示,为所有可能的输入来建立确定的程序的运行状况。

系统的形式化验证要求使用精确数学含义的语言描述的一个程序及其所需行为(即,规范)的抽象模型。这个规范可能是完整的,或者它可能被限定到特定的程序属性:

——功能正确性属性,即程序应当显示一个特定的功能;

——安全(即一些不好的运行状况永远不会发生)和活性(即一些好的运行状况最终会发生)属性;

——时间属性,即一些运行状况将在特定时间发生。

形式化验证的结果是一项严密的论证:针对所有可能的输人,与该规范有关的程序的抽象模型是正确的。即模型满足特定的属性。

但是,该模型的正确性并不直接证明实际程序的正确性,需进一步说明:针对关心的属性,该模型是一个实际程序的精确抽象。一些实际关心的程序属性不能以数学方法形式化(例如大多数计时和调度，或主观的属性。例如“清晰而简单的”用户接口,或者确实不易用形式化语言表达的任何属性或设计目标)。因此形式化验证不会完全取代模拟和测试,而是针对所有的输入,通过提供进一步的证据来支持程序的正确运行来补充这些技术。当形式化验证可以确保程序的抽象模型的正确性时,通过测试来保证实际期望的程序运行状况。

在设计阶段,形式化验证的使用可能通过在设计阶段的早期发现重大错误和疏忽来大大减少开发时间,从而减少了设计与测试间迭代的时间。

一些实际应用中的形式化方法在C.2.4中有描述:例如,CCS,CSP,HOL,LOTOS,OBJ,时序逻辑， VDM和 Z。