这次我将要写的主题并不是一个简单的问题。我将尝试解释为什么形式化验证是更好的选择。尤其是为什么在验证铁路系统的安全需求时使用形式化验证是一种好的做法。
验证问题
为了做出令人信服的论证，我需要从头开始。这一切都始于系统和系统应该满足的一些安全需求。我们假设系统是联锁，联锁系统是否满足了人为设定的安全需求，这可以称为验证问题。
让我们考虑一下验证问题。需要做什么？我们所拥有的是联锁软件和一些安全需求。为了方便理解，我们假设联锁软件由许多布尔变量组成。其中一些变量是输入，一些是输出，一些（可能是最多）是内部或中间变量。然后，以这些变量赋值来表示联锁系统潜在的状态空间（state space）。所有可能赋值组合的集合则代表了系统的全部潜在状态空间。运行联锁系统一个或者多个周期，意味着从一个状态转移到另一个状态。此外，一些状态对应于系统启动时需要完成的变量赋值。这些被称为初始状态（initial states）。可达状态（reachable states）是可以从初始状态出发，通过运行联锁系统可到达的状态集合。一般情况下，可达状态只是潜在状态空间的一小部分。
什么是安全需求？
什么是安全需求（safety requirements）？安全需求对应于不应该发生的事件。从本质上讲，安全需求是联锁不应该去实现的一个或多个变量的赋值。也就是说，安全需求定义了系统不应该到达的状态的集合，因为这些状态是系统出现安全问题和事故时的状态。因此，一个联锁系统的验证问题归结为以某种令人信服的方式去表明安全需求所定义的状态空间不包含该联锁的任何可达状态。
这件事看上去似乎不是那么难。
Hmmm，实际上确实很难。
主要原因是任何真实有用的系统的潜在状态空间都非常巨大。
如果我们只考虑布尔变量，
则系统空间包含2 ^ {变量数量} 个潜在状态。
如果联锁包含100个布尔变量，则潜在的状态空间具有
1 267 650 600 228 229 401 496 703 205 376，约10 ^ 30个状态！
相比之下，地球上的树木数量估计为3 * 10 ^ 12。这只是100个变量，这代表了一个非常小的联锁系统。
现在大家应该能同意了，没有手动方法可以完全解决验证问题。测试当然也不行。要通过测试获得百分百覆盖，必须尝试输入变量值的所有可能组合，然后仿真系统以验证没有违反安全需求。但即使假设输入变量的数量是100，那么要在1年内完成测试，则需要每秒完成4 * 10 ^ 22个测试用例，这还没考虑执行路径上输入的时序变化组合。显然通过测试去做完全验证是不可行的。
那么验证问题的解决方案是什么？
我们下次再谈……