如果您已经阅读了本系列的前两部分（在此处阅读第1部分，在此处阅读第2部分），那么您将知
道，验证联锁满足安全要求并不是一件容易的事。由于联锁的状态空间很大，因此手动方法和测
试都无法助您一臂之力。您还知道数学是寻找我们所需要方法的地方。所以最后我们可以开始谈
论形式验证了。
与科学一样，为了将验证问题转移到数学领域，我们对所涉及部分进行数学模型化：联锁和安全
需求。可以为我们提供适当方法和概念的数学部分是逻辑。我们想知道的是如下内容：
当联锁命令显示允许信号时，是否有从该信号开始的锁定路线？
我们要提供令人信服的，严谨的论据，以表明这种声明是正确的，即我们想要证明这一点。数理
逻辑做为数学的一部分可以为我们提供答案。在那里，“真相”，“陈述”和“证明”之类的概念被赋予
了精确的含义。问题的核心是对此类问题进行数学处理：
陈述A的真相是否使得陈述B的真相？
或者，幸运的是，同一件事，
是否存在从陈述A到陈述B的证明？
而这正是我们解决验证问题所需的数学。
在形式验证中，我们要做的是建立联锁的逻辑模型（我们的陈述A）和另一个安全要求模型（我们
的陈述B）。因此，我们设法将验证问题转化为数学问题，这意味着如果我们能够从陈述A得出陈
述B的证明，则实际上就已经证明联锁满足安全要求，也就是我们已经证明联锁永远不会进入违反
安全需求的状态。
因此，从理论上讲，这个方法一切都很好。在实践中行得通吗？
幸运的是，它在实践中也是可行了。原因是最重要的任务可以由计算机工具完成。特别是，有些
计算机工具可以从语句A中找到语句B的证明。当涉及建模部分时，最大的任务是联锁的建模。但
是，也可以通过类似于编译器的计算机工具来完成此任务，将联锁程序转换为逻辑模型，并保留
原始程序的所有重要方面。需求建模通常是手工完成的，但是可以在通用部分和特定部分中完
成。然后将这些信息输入到证明工具中，该工具专门针对要验证的特定应用并满足通用需求。因
此，通用需求可以重新用于其它联锁，从而将花费在需求建模上的时间最小化。
该博客总结了一系列博客，回答了为什么形式验证是解决验证问题的方法，希望是充满说服力的
，或至少引起您的好奇。