ACM通信
研究突出了
技术角度:Ironfleet简化了安全性和活跃性的验证
就像关于美的主张一样，关于系统正确性的主张是相对于期望的。对计算系统的这种期望称为规范。虽然关于美的断言必然是主观的(“在旁观者的眼里”)，但关于正确性的断言不一定——它们可以作为形式逻辑的证明来传达，可以传达给任何人，然后独立地进行检查。
一个给定的正确性声明是否有用将取决于该规范如何完整地描述系统的行为。显然，我们受到了使用规范语言可以说什么以及使用形式逻辑可以证明什么规范的限制。在过去的半个世纪里，人们达成了一种共识，即指定一系列行为称为跟踪属性是一个甜蜜点。跟踪属性足以描述系统行为的大多数重要方面。此外，系统的跟踪属性可以直接从其组件的跟踪属性中推导出来，因此我们可以组合地推理跟踪属性。
根据定义，跟踪属性的描述必须描述一组系统行为，其中系统行为a是否包含在该集合中仅取决于a，而不取决于该集合中的其他系统行为或该集合的其他属性。因此，迹属性形式化了部分正确性和完全正确性、互斥性、死锁自由、饥饿自由等等。
此外，跟踪属性很容易指定。程序的文本指定一个包含该程序可能执行的集合的跟踪属性，因为执行可能取决于之前发生的事情，而不取决于不同执行中发生的事情。通过将系统行为建模为状态和/或动作的序列，自动机可以用来指定由自动机接受的序列组成的跟踪属性。线性时时间逻辑的公式或它的导数如TLA是由单个序列满足的，因此满足一个给定公式的序列集也是一个迹性。
在1977年的一篇论文中，莱斯利·兰波特使用了这些术语安全属性(“不好的事情”不会发生)和活性属性(“好事”确实发生了)，与互斥协议和其他并发算法的推理有关。
这两种规格似乎涵盖了整个景观。在接下来的十年里，阿尔彭和我证明了兰波特是对的。我们证明了安全属性和活性属性是所有痕量属性的基本构建模块;不变量足以验证安全属性;还需要变量函数来验证活性属性。因此，不仅安全属性和活性属性是指定程序行为的自然方式，而且这样的分解提供了构建证明所需的方法的洞察力。
理论上是这样的。下面的论文代表着实践向前迈出的重要一步。它描述了两个非平凡分布式服务的机械检验证明:一个支持复制的基于paxos的库和一个共享的键值存储。证明了它们的适当安全性能和活性性能。这些并不是对非平凡系统软件的第一个机械检验证明。但之前的工作只是证明了安全属性，其中不变量就足够了;必须使用其他技术(如上所述)来证明活性属性。
IronFleet很有趣，因为它使用细化和简化来简化证明结构。
IronFleet也很有趣，因为它使用细化和简化来简化证明结构。细化是一种方式，表明满足低层次规范的系统满足了某些高级规范;约简允许对粗粒度原子操作进行推理，以支持对具有细粒度操作的系统的推理。这些技术并不新鲜，但是通过IronFleet，我们可以在真实的系统软件中看到它们的作用。例如，我们看到如何通过限制服务可能采取的每个单独步骤的内部设计来避免证明活性属性的简化困难。因此，我们了解了一个工程工作，它必须包含系统建设和证明建设。
作者还报告了性能影响和代码大小的扩展，以适应机械证明检查所需的注释。
我们现在更接近于有能力使软件系统伴随着基于机械检查证明的正确性声明。需求是巨大的;这里所报告的进展应该是一种鼓舞。
数字图书馆是由计算机协会出版的。版权所有©2017 ACM, Inc.
没有发现记录