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 article 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 [ 26 ]. The “sequence maps” are then shown to provide an alternative representation of deterministic state machines and 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 logic or other foundational 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.

The C programming language was developed in the 1970s as a fairly unconventional systems and operating systems development tool, but has, through the course of the ISO Standards process, added many attributes of more conventional programming languages and become less suitable for operating systems development. Operating system programming continues to be done in non-ISO dialects of C. The differences provide a glimpse of operating system requirements for programming languages.

The authors use the modal primitive recursive (MPR) arithmetic to facilitate definition, composition, and reasoning about the very large-scale finite state machines that represent substantive real-time systems. The MPR arithmetic provides a language of integer-valued functions which allow for compact and intuitive specification of state machines without enumeration of state sets or transition functions. The MPR arithmetic proof system is intended to be as close as possible to the proof system of classical algebra. The expressive range of the language extends from detailed description of multilevel concurrent algorithms to abstract properties of liveness and safety in a style similar to that of the temporal logics. The behavior of a real-time priority queue or communication pipeline is specified with MPR as an example, and the correctness of an implementation is verified.>