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控制器在内的多个简化示例。