In this paper, we pursue the goal of automatic deductive verification for certain classes of ASM. In particular, we base our work on a translation of general ASMs to full first-order temporal logic. While such a logic is, in general, not finitely axiomatisable, recent work has identified a fragment, termed the monodic fragment, that is finitely axiomatisable and many of its subfragments are decidable. Thus, in this paper, we define a class of monodic ASMs whose semantics in terms of temporal logic fits within the monodic fragment. This, together with recent work on clausal resolution methods for monodic fragments, allows us to carry out temporal verification of monodic ASMs. The approach is illustrated by the deductive verification of FloodSet algorithm for Consensus problem, and Synapse N+1 cache coherence protocol; both are specified by monodic ASMs.
展开▼
机译：在本文中，我们追求针对某些类别的ASM进行自动演绎验证的目标。特别是，我们的工作基于将通用ASM转换为完整的一阶时间逻辑。虽然这样的逻辑通常不是有限公理的，但是最近的工作已经确定了一个片段，称为单齿片段，它是有限公理的，并且其许多子片段是可确定的。因此，在本文中，我们定义了一类单调ASM，其时间逻辑方面的语义适合单调片段。这，再加上最近关于单片碎片的子句解决方法的工作，使我们能够对单片ASM进行时间验证。通过对共识问题的FloodSet算法的演绎验证和Synapse N + 1缓存一致性协议来说明该方法。两者均由单向ASM指定。
展开▼
