Analysis of parallel systems.

A formal analysis procedure for hardware and software computer systems is described. A system is described by a flow table model. The concept of an output hazard is introduced to account for effects of unbounded line delays. Necessary and sufficient conditions for the absence of output hazards are given. A system that contains no output hazards is said to operate correctly if the system state graph that describes all system states and state transitions is free from forbidden states and forbidden state sequences. A flow table solution for the two-component mutual exclusion problem is analyzed and shown to be correct.