The main aim of this report is to provide an introductory tutorial on the Abstract State Machines (ASM) specification method for software engineering to an audience already familiar with the Temporal Logic of Actions (TLA$^+$) method. The report asks to what extent the ASM and TLA$^+$ methods are complementary in checking specifications against stated requirements and proposes some answers. A second aim is to provide a comparison between different executable frameworks that have been developed for the same specification languages. Thus, the ASM discussion is complemented by executable Corinthian ASM (CASM) and CoreASM models. Similarly, the two TLA$^+$ specifications presented, which rely on the TLC and Apalache model checkers, respectively, are complemented by a Quint specification, a new language developed by Informal Systems to serve as a user-friendly syntax layer for TLA$^+$. For the basis of comparison we use the specification of the Alternating Bit (AB) protocol because it is a simple and well-understood protocol already extensively analysed in the literature. While the models reported here and developed with the two methods are semantically equivalent, ASMs and Quint are better suited for top-down specification from abstract requirements by iterative refinement. TLA$^+$ seems to be more easily used bottom-up, to build abstractions on top of verified components in spite of the fact that it, too, emphasizes iterative refinement. In the final section, the report begins to scope out the possibility of a homomorphism between the specification of the AB protocol and its finite-state machine (FSM) through state space visualizations, motivated by a search for a formal decomposition method.

翻译：本报告的主要目的是为已熟悉动作时序逻辑（TLA$^+$）方法的读者，提供关于软件工程中抽象状态机（ASM）规范方法的入门教程。报告探讨了ASM和TLA$^+$方法在根据既定需求检查规范方面的互补程度，并提出了一些答案。第二个目的是比较为相同规范语言开发的不同可执行框架。因此，对ASM的讨论辅以可执行的科林斯ASM（CASM）和CoreASM模型。类似地，本文介绍的两个TLA$^+$规范分别依赖于TLC和Apalache模型检查器，并辅以Quint规范——这是Informal Systems开发的一种新语言，旨在作为TLA$^+$的用户友好语法层。我们以交替比特（AB）协议的规范作为比较基础，因为这是一个简单且已被广泛分析的经典协议。尽管本文报告并采用两种方法开发的模型在语义上等价，但ASM和Quint更适合通过迭代细化从抽象需求进行自顶向下的规范。而TLA$^+$似乎更易于自底向上使用，即在已验证组件之上构建抽象——尽管它同样强调迭代细化。在最后一节中，受形式化分解方法的启发，本报告通过状态空间可视化，初步探讨了AB协议规范与其有限状态机（FSM）之间同态的可能性。