A logic-free method for modular composition of specifications

Abstract

Clear mathematical description of large scale digital systems is not possible without extensive use of encapsulation. We argue that standard models of concurrency and composition are too unstructured to support modular composition and verification of systems. We offer an alternative model based on algebraic feedback products of finite state machines. We also describe a technique for concisely specifying complex state machines in terms of state dependent (modal) functions. The product automata model provides a precise interpretation for the formal expressions, and the formal expressions provide an intuitive language for describing multi-layer concurrent digital systems. We develop several examples, showing how specifications of varying levels of abstractness can be composed to specify rather complex systems.