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. The main finding is that while the two methods appear to be semantically equivalent ASMs are better suited for top-down specification from abstract requirements by iterative refinement, whereas TLA$^+$ is often used more 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的讨论辅以可执行的Corinthian ASM（CASM）和CoreASM模型。类似地，文中所呈现的两个TLA$^+$规约（分别依赖TLC和Apalache模型检查器）则辅以Quint规约——这是Informal Systems开发的一种新语言，旨在作为TLA$^+$的友好语法层。作为比较基础，我们选用交替比特（AB）协议的规约，因为该协议简单且已被文献广泛分析。主要发现是：尽管两种方法在语义上看似等价，但ASM更适合通过迭代精化从抽象需求进行自顶向下规约，而TLA$^+$虽也强调迭代精化，却常被用于自底向上构建已验证组件的抽象。在最后章节，受形式化分解方法研究的驱动，报告通过状态空间可视化初步探讨了AB协议规约与其有限状态机（FSM）之间同态映射的可能性。