Specifying and verifying a real-time priority queue with modal algebra

Abstract

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.