Specifications of complex, large scale, computer software and hardware systems can be radically simplified by using simple maps from input sequences to output values. These "state machine maps" provide an alternative representation of classical Moore type state machines. Composition of state machine maps corresponds to state machine products and can be used to specify essentially any type of interconnection as well as parallel and distributed computation. State machine maps can also specify abstract properties of systems and are significantly more concise and scalable than traditional representations of automata. Examples included here include specifications of producer/consumer software, network distributed consensus, real-time digital circuits, and operating system scheduling. The motivation for this work comes from experience designing and developing operating systems and real-time software where weak methods for understanding and exploring designs is a well known handicap. The methods introduced here are based on ordinary discrete mathematics, primitive recursive functions and deterministic state machines and are intended, initially, to aid the intuition and understanding of the system developers. Staying strictly within the boundaries of classical deterministic state machines anchors the methods to the algebraic structures of automata and semigroups, obviates any need for axiomatic deduction systems, "formal methods", or extensions to the model, and makes the specifications more faithful to engineering practice. While state machine maps are obvious representations of state machines, the techniques introduced here for defining and composing them are novel. To illustrate applications, the paper includes a fairly detailed specification and verification of the well-known "Paxos" distributed consensus algorithm plus a number of simpler examples including a digital PID controller.

翻译：通过使用从输入序列到输出值的简单映射，复杂大规模计算机软件与硬件系统的规约可被极大简化。这种"状态机映射"为经典摩尔型状态机提供了替代性表示。状态机映射的组合对应着状态机乘积，可规约几乎所有类型的互联结构以及并行与分布式计算。状态机映射还能规约系统的抽象属性，且相较于传统自动机表示具有显著更高的简洁性与可扩展性。本文示例涵盖生产者/消费者软件规约、网络分布式共识、实时数字电路及操作系统调度。本工作的动机源于操作系统与实时软件的设计开发经验——在这些领域，理解与探索设计的薄弱方法已成为公认瓶颈。本文方法建立于普通离散数学、原始递归函数及确定性状态机基础之上，初始目标在于辅助系统开发者的直觉认知与理解。严格限定于经典确定性状态机框架，使该方法扎根于自动机与半群代数结构，既无需依赖公理演绎系统、"形式化方法"或模型扩展，又使规约更贴合工程实践。尽管状态机映射是状态机的显式表示，本文提出的定义与组合方法具有创新性。为展示应用，论文包含对著名"Paxos"分布式共识算法的详细规约与验证，以及包括数字PID控制器在内的若干简化实例。