Using Fairness to Make Abstractions Work
Using Fairness to Make Abstractions Work
复制标题
使用公平性使抽象发挥作用
作者：
D. Bosnacki;N. Ioustinova;N. Sidorova
抽象常常会引入无限的痕迹，这些痕迹在具体层面上没有相应的痕迹，并可能导致验证失败。细化并不总是有助于消除这些痕迹。在本文中，我们考虑了一种计时器抽象，它在抽象计时器上引入了循环行为，并展示了如何通过对抽象模型施加强公平性约束来排除循环。利用抽象定时器上的循环是自循环的事实，我们将强公平约束转化为弱公平约束，并将其嵌入到验证算法中。我们在 DTSpin 模型检查器中实现了该算法，并在案例研究中展示了其效率。相同的方法可用于引入自循环的其他数据抽象。
Abstractions often introduce infinite traces which have no corresponding traces at the concrete level and may lead to failure of the verification. Refinement does not always help to eliminate those traces. In this paper, we consider a timer abstraction that introduces a cyclic behaviour on abstract timers and we show how one can exclude cycles by imposing a strong fairness constraint on the abstract model. By employing the fact that the loop on the abstract timer is a self-loop, we render the strong fairness constraint into a weak fairness constraint and embed it into the verification algorithm. We implemented the algorithm in the DTSpin model checker and showed its efficiency on case studies. The same approach can be used for other data abstractions that introduce self-loops.