Proving refinement using transduction
Proving refinement using transduction
复制标题
使用转导证明精化
作者：
B. Jonsson;A. Pnueli;C. Rump
总结。在设计分布式系统时，人们面临着验证在不同抽象层次给出的两个规范之间的细化问题。文献中提出的验证技术包括细化映射和各种形式的模拟。我们提出一种验证方法，通过构建一个转换器来证明两个系统之间的细化，该转换器输入一个具体系统的计算并输出一个与之匹配的抽象系统的计算。转换器使用一个先进先出队列，该队列保存尚未匹配的具体计算片段。这允许在具体事件发生和相应抽象事件确定之间存在有限的延迟。这种延迟通常使得预言变量或反向模拟的使用变得不必要。
该方法的一个重要推广是在对观察到的事件序列进行某种变换的情况下证明细化。通过用一个允许对事件序列进行适当变换的组件替换先进先出队列来调整该方法。一个特殊情况是偏序细化，即仅保留系统事件之间部分顺序的细化。例如顺序一致性和可串行化。在一个缓存协议的顺序一致性证明中说明了顺序一致性的情况。
Summary. When designing distributed systems, one is faced with the problem of verifying a refinement between two specifications, given at different levels of abstraction. Suggested verification techniques in the literature include refinement mappings and various forms of simulation. We present a verification method, in which refinement between two systems is proven by constructing a transducer that inputs a computation of a concrete system and outputs a matching computation of the abstract system. The transducer uses a FIFO queue that holds segments of the concrete computation that have not been matched yet. This allows a finite delay between the occurrence of a concrete event and the determination of the corresponding abstract event. This delay often makes the use of prophecy variables or backward simulation unnecessary.
An important generalization of the method is to prove refinement modulo some transformation on the observed sequences of events. The method is adapted by replacing the FIFO queue by a component that allows the appropriate transformation on sequences of events. A particular case is partial-order refinement, i.e., refinement that preserves only a subset of the orderings between events of a system. Examples are sequential consistency and serializability. The case of sequential consistency is illustrated on a proof of sequential consistency of a cache protocol.