Verification of Process Structures of Interacting Digital Systems

Abstract

A formal, universe for systems design has been developed, in which representations of interacting digital, systems are interpreted by a deterministic automaton acting on state information in the form of character strings. Since process structures in this universe can be described with regular languages, a new interpretation is defined in which regular languages represent state information. Computations under this new hterpretation contain the previous ones (with some loss of detail), making it possible to prove assertions about the origina1 string computations. An example is given to show the formulation, and algorithmic verification, of some interesting properties of two asynchronous communicating systems.