Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

State machines for large scale computer software and systems

Victor Yodaiken

TL;DR

The paper addresses the challenge of scaling state-machine specifications for large-scale software and systems without resorting to axiomatic formal methods. It introduces primitive recursive sequence maps and Moore-machine representations as constructive, compositional tools for defining and analyzing deterministic state behavior, with $f_M(w)$ capturing the output after sequence $w$. Through detailed development of composition (direct product, embedding, general product) and Moore-machine products, the framework enables concise, modular specifications and rigorous reasoning about interconnected, parallel, and real-time systems. The Paxos distributed consensus protocol is used as a substantial validation example, where local rules and network models yield a safety proof that all winning proposals share the same value. The work bridges automata theory and practical system design, offering a scalable, algebraic approach that supports design verification prior to implementation and informs modularity, interconnection, and scheduling decisions in large-scale systems.

Abstract

The behavior and architecture of large scale discrete state systems found in computer software and hardware can be specified and analyzed using a particular class of primitive recursive functions. This paper begins with an illustration of the utility of the method via a number of small examples and then via longer specification and verification of the Paxos distributed consensus algorithm. The sequence maps are then shown to provide an alternative representation of deterministic state machines and algebraic products of state machines. Distributed and composite systems, parallel and concurrent computation, and real-time behavior can all be specified naturally with these methods - which require neither extensions to the classical state machine model nor any axiomatic methods or other techniques from formal methods. Compared to state diagrams or tables or the standard set-tuple-transition-maps, sequence maps are more concise and better suited to describing the behavior and compositional architecture of computer systems. Staying strictly within the boundaries of classical deterministic state machines anchors the methods to the algebraic structures of automata and makes the specifications faithful to engineering practice.

State machines for large scale computer software and systems

TL;DR

The paper addresses the challenge of scaling state-machine specifications for large-scale software and systems without resorting to axiomatic formal methods. It introduces primitive recursive sequence maps and Moore-machine representations as constructive, compositional tools for defining and analyzing deterministic state behavior, with capturing the output after sequence . Through detailed development of composition (direct product, embedding, general product) and Moore-machine products, the framework enables concise, modular specifications and rigorous reasoning about interconnected, parallel, and real-time systems. The Paxos distributed consensus protocol is used as a substantial validation example, where local rules and network models yield a safety proof that all winning proposals share the same value. The work bridges automata theory and practical system design, offering a scalable, algebraic approach that supports design verification prior to implementation and informs modularity, interconnection, and scheduling decisions in large-scale systems.

Abstract

The behavior and architecture of large scale discrete state systems found in computer software and hardware can be specified and analyzed using a particular class of primitive recursive functions. This paper begins with an illustration of the utility of the method via a number of small examples and then via longer specification and verification of the Paxos distributed consensus algorithm. The sequence maps are then shown to provide an alternative representation of deterministic state machines and algebraic products of state machines. Distributed and composite systems, parallel and concurrent computation, and real-time behavior can all be specified naturally with these methods - which require neither extensions to the classical state machine model nor any axiomatic methods or other techniques from formal methods. Compared to state diagrams or tables or the standard set-tuple-transition-maps, sequence maps are more concise and better suited to describing the behavior and compositional architecture of computer systems. Staying strictly within the boundaries of classical deterministic state machines anchors the methods to the algebraic structures of automata and makes the specifications faithful to engineering practice.

Paper Structure

This paper contains 33 sections, 16 theorems, 59 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Introduction to applications and method
  3. Shift register and connection maps
  4. A controller for a physical plant
  5. A system of interconnected processes
  6. The Paxos protocol
  7. Packet network
  8. Paxos
  9. Proof sketch
  10. Discussion
  11. Primitive Recursive Sequence Functions and State Machines
  12. Standard Representation of Moore Machines
  13. Characteristic function of a Moore machine tuple
  14. Sequence primitive recursion
  15. Finite state machines
  16. ...and 18 more sections

Key Result

Lemma 1

If $G$ is a network agent with identifier $i$ and $m\in \mathit{Sent}(G, q)$ then $source(m)=i$.

Figures (9)

  • Figure 1: Sequence maps representing state machines
  • Figure 2: The general product
  • Figure 3: Shift register
  • Figure 4: Direct product of sequence maps
  • Figure 5: An abstract process
  • ...and 4 more figures

Theorems & Definitions (28)

  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Lemma 1
  • Definition 3.4
  • Lemma 2
  • Lemma 3
  • Definition 3.5
  • Theorem 1
  • Definition 4.1
  • ...and 18 more