Fei

如果您已经阅读了本系列的前两部分，那么您将知道，验证联锁满足安全要求并不是一件容易的事。由于联锁的状态空间很大，因此手动方法和测试都无法助您一臂之力。

“形式化”其实就是指“数学”。因此，形式验证意味着将验证问题转化为数学问题。大家都知道一旦连结到数学领域，我们就可以获得数学所带来的严谨性和精确性。

我将尝试解释为什么形式化验证是更好的选择。尤其是为什么在验证铁路系统的安全需求时使用形式化验证是一种好的做法。 为了做出令人信服的论证，我需要从头开始。