Johnson This research is on developing formal techniques to decompose higher-level system specifications into interacting sequential processes. A functional algebra is used for defining formal representations and building a set of transformations for manipulating them. The notion of "interaction schemes" is the central subject. The project is composed of four activities: 1. theoretical studies of the decomposition of digital systems; especially formal derivation of control-synchronization and data- communication protocols; 2. automation of formal transformations which correctly do sequential decompositions; 3. integration of the mechanized formal system with available CAD tools, and other reasoning systems; and 4. application of the design system to meaningful examples of digital-system designs.
