形式验证

为什么进行形式验证-验证问题的解决方案

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

By |2020-03-31T09:31:17+01:00四月 14th, 2020|形式验证|

形式化验证Why系列之二:形式化验证的适用性

希望您已阅读本系列的第1部分,在那里您可以发现传统方法在验证铁路联锁的安全需求时不是很给力。 这次我的任务是说服大家形式化验证是一个更好的选择。 那么什么是形式化验证呢? 好吧,我们已经知道验证意味着什么。 “形式化”其实就是指“数学”。因此,形式验证意味着将验证问题转化为数学问题。大家都知道一旦连结到数学领域,我们就可以获得数学所带来的严谨性和精确性。 数学中的典型活动是发表陈述或声明(statements),然后证明(prove)它们是真实或成立的。听起来很熟悉?数学陈述的证明必须是令人信服的,无懈可击的,任何受过适当教育的人看过证明过程后都应该同意陈述是真的。当然,在实践中,最后一部分可能会难以实现。即使接受适当的教育,数学的某些部分也很难理解。但让我们考虑一个算术的经典例子。考虑如下声明: 1 + 2 + ... + n = n(n + 1)/2 看我的答案之前请考虑几秒钟,看看你能否想到证明方法。 Hmmm... 在我看来,最优雅的证明方法,是在把等式左侧连续写两次,每次写数字序列的方向不同。比如: 1 +       2 + ... + n n + (n-1) + ... + 1 请注意,数字的顺序在较低的一行中是倒序。如果我们查看此表达式中的列,每列的总和为 n+1,并且有n 列。因此,所有这两行数字相加总和是 n(n + 1) 然后我们就得到了如下的结果 2(1 + 2 + ... + n)= n(n + 1) 这意味着 1 + 2 + [...]

By |2020-03-31T09:24:29+01:00四月 7th, 2020|形式验证|

形式化验证Why系列之一:铁路系统的安全需求

这次我将要写的主题并不是一个简单的问题。我将尝试解释为什么形式化验证是更好的选择。尤其是为什么在验证铁路系统的安全需求时使用形式化验证是一种好的做法。 验证问题 为了做出令人信服的论证,我需要从头开始。这一切都始于系统和系统应该满足的一些安全需求。我们假设系统是联锁,联锁系统是否满足了人为设定的安全需求,这可以称为验证问题。 让我们考虑一下验证问题。需要做什么?我们所拥有的是联锁软件和一些安全需求。为了方便理解,我们假设联锁软件由许多布尔变量组成。其中一些变量是输入,一些是输出,一些(可能是最多)是内部或中间变量。然后,以这些变量赋值来表示联锁系统潜在的状态空间(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个测试用例,这还没考虑执行路径上输入的时序变化组合。显然通过测试去做完全验证是不可行的。 那么验证问题的解决方案是什么? 我们下次再谈......

By |2020-03-31T09:19:19+01:00三月 31st, 2020|形式验证|