演绎验证与模型检验的取舍

形式化方法除了规约语言和开发方法，还需要相应的验证技术，主要分演绎验证和模型检验两大类，二者代表了两种截然相反的取舍。演绎验证先建立一套逻辑系统，再从公理和验证规则出发推导系统模型是否满足特定性质——优点是既能用于有穷状态也能用于无穷状态、甚至能处理参数化程序（如任意数目相同进程的程序），验证过程往往由代码开发者以外的人来完成，这本身有助于增加理解程序算法背后直观内容的人数、从而提高发现错误的概率；但缺点也很突出：验证过程不能全自动进行，需要人的参与，非常耗时，可能成为大型项目的瓶颈，速度明显慢于测试和模型检验；演绎验证大部分手动完成，极度依赖验证人员的智慧和数学背景，且验证人员常常倾向于给被验证域添加一些看似简单实则限制了证明一般性的假设，并错误地把这些假设当成公理使用。模型检验通过对有穷状态空间的穷尽搜索，自动检查系统模型是否满足给定性质——优点是整个搜索过程完全自动化，基于相对容易实现的技术、已有大量成熟工具，发现不满足的属性时能给出违反执行的反例、便于调试；缺点是只能处理有穷状态系统，面对无穷或复杂系统容易出现”状态空间爆炸”问题（例如n个相互异步的进程、每个进程m个状态，总状态数就是m的n次方），而且检验前通常需要把待验证程序手动抽象成有限状态系统，一旦模型检验发现”错误”，往往还得手工确认这是真实错误还是原始程序和抽象模型之间不一致产生的误报。两者的核心取舍是”自动化程度”与”表达能力”的互换：演绎验证能处理更广泛的状态空间和参数化场景，代价是几乎无法自动化；模型检验能完全自动跑完整个验证，代价是被限制在有穷状态、且面临组合爆炸的规模天花板。