A modal arithmetic for reasoning about multilevel systems of finite state machines

This dissertation advances a novel approach to formal specification and verification of systems-level computation. The approach is based on a purely finite state model of computation, and makes use of algebraic and syntactic techniques which have not been previously applied to the problem. The approach makes use of a modal extension of the primitive recursive functions to specify system behavior, and uses an algebraic feedback product of automata to provide semantic content for specifications. The modal functions are shown to provide highly compact and expressive notation for defining, composing, and verifying the properties of large-scale finite state machines. The feedback product allows for a very general model of composition, multi-level dynamic behavior, and concurrency. Techniques are developed for specifying both detailed operation of algorithms, and abstract system properties such as liveness and safety. Several significant examples are provided to illustrate application of the method to complex algorithms and designs