抽象状态机

在计算机科学中，抽象状态机（ASM）是一种在任意数据结构（数理逻辑意义上的结构，即一个非空的集合以及该集合上的一些函数（操作）和关系）上运行的状态机。

ASM方法是一种实用的、有科学依据的系统工程方法，在系统开发的两端之间架起了桥梁。该方法建立在三个基本概念之上。ASM：一种精确的伪代码形式，概括了有限状态机以在任意数据结构上运行地面模型：一种严格的蓝图形式，作为设计的权威参考模型完善：一种最通用的方案，用于将模型抽象逐步实例化为具体的系统元素，在系统开发的连续阶段提供越来越详细的描述之间的可控联系。在ASM的最初概念中，单个代理按一系列步骤执行程序，可能与环境交互。这个概念被扩展到捕捉分布式计算，在这种情况下，多个代理同时执行其程序。由于ASM在任意的抽象层次上对算法进行建模，它们可以提供硬件或软件设计的高层次、低层次和中层次视图。ASM规格通常由一系列的ASM模型组成，从抽象的基础模型开始，在连续的细化或粗化中进入更高的细节水平。由于这三个概念的算法和数学性质，ASM模型及其感兴趣的属性可以使用任何严格的验证形式（通过推理）或验证（通过实验、测试模型的执行）进行分析。

ASM的概念要归功于YuriGurevich，他在80年代中期首次提出，作为改进图灵关于每个算法都由适当的图灵机模拟的论文的一种方式。他提出了ASM理论：每一种算法，无论多么抽象，都能被适当的ASM一步步地模拟。2000年，Gurevich将顺序算法的概念公理化，并为其证明了ASM论文。粗略地说，公理如下：状态是结构，状态转换只涉及状态的有界部分，一切在结构的同构下是不变的。(结构可以被看作是代数，这就解释了ASM最初的名字是演化代数)。

顺序算法的公理化和特征化已被扩展到并行和交互式算法。在20世纪90年代，通过社区的努力，ASM方法被开发出来，使用ASM对计算机硬件和软件进行形式化规范和分析（验证和确认）。编程语言（包括Prolog、C和Java）和设计语言（UML和SDL）的全面ASM规范已经被开发出来。详细的历史记录可以在其他地方找到。一些用于ASM执行和分析的软件工具已经问世。