形式验证可以应用于任何类型的软件,还是仅某些类型适用?

任何软件都可以进行正式验证,但这很辛苦。 这就是为什么它很少做的原因。

直到最近才可以对非确定性流程进行正确建模,但此后对其进行了分类。 即使这样,也很难。 这就是SEL4没有网络的原因。 因为可以将池用于动态数据,所以可以证明软件是正确的(因为运行期间环境不会改变),但实际上所有验证都针对静态数据对象是如此困难。

考虑到软件的设计,正式验证会更容易。 定义明确的点处的定义明确的条件意味着您可以总结这些点之间的状态变化,并查看总和加上起点是否等于终点。 Sane人使用软件检查器执行此操作,而疯狂的人则在纸上使用旧方法执行此操作。 旧方法每十行大约需要一天。