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.

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