Unreliable Channels are Easier to Verify Than Perfect Channels
Unreliable Channels are Easier to Verify Than Perfect Channels
复制标题
不可靠的渠道比完美的渠道更容易验证
作者：
Gérard Cécé;A. Finkel;S. Iyer
我们考虑的问题验证的正确性有限状态机，相互通信的无界FIFO通道是不可靠的。Finkel、Abdulla和Jonsson已经考虑了在FIFO通道的验证中可能丢失消息的各种感兴趣的问题。在本文中，我们考虑了通信信道的其他可能的不可靠行为，即，(a)重复和（B）插入错误。此外，我们还考虑了各种组合的重复，插入和损失错误。通过无界FIFO缓冲器进行通信的有限状态机是一种计算模型，它构成了ISO标准协议规范语言Estelle和SDL的主干。虽然一个完美的通信介质的假设是合理的，在较高层次的OSI协议栈，较低的层次必须处理一个不可靠的通信介质，因此我们的动机，目前的工作。感兴趣的验证问题是可达性，无界性，死锁和模型检查对CTL*。所有这些问题对于在可靠的无界FIFO通道上通信的机器来说都是不可判定的。因此，当对不可靠的信道进行建模时，这些问题中的一些变得可判定，这可能是令人惊讶的。本文的贡献是：（a）调查这些问题的解决方案的机器与插入错误，复制错误，或复制，插入和lossiness错误的组合，和（B）的各种错误的相对表达能力的比较。
We consider the problem of verifying correctness of finite state machines that communicate with each other over unbounded FIFO channels that are unreliable. Various problems of interest in verification of FIFO channels that can lose messages have been considered by Finkel and by Abdulla and Jonsson. We consider, in this paper, other possible unreliable behaviors of communication channels, viz., (a) duplication and (b) insertion errors. Furthermore, we also consider various combinations of duplication, insertion, and lossiness errors. Finite state machines that communicate over unbounded FIFO buffers are a model of computation that forms the backbone of the ISO standard protocol specification languages Estelle and SDL. While the assumption of a perfect communication medium is reasonable at the higher levels of the OSI protocol stack, the lower levels have to deal with an unreliable communication medium; hence our motivation for the present work. The verification problems that are of interest arereachability,unboundedness,deadlock, andmodel-checking against CTL*. All of these problems are undecidable for machines communicating over reliable unbounded FIFO channels. So it is perhaps surprising that some of these problems become decidable when unreliable channels are modeled. The contributions of this paper are (a) an investigation of solutions to these problems for machines with insertion errors, duplication errors, or a combination of duplication, insertion, and lossiness errors, and (b) a comparison of the relative expressive power of the various errors.