Abstract :
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.
Keywords :
Determinancy, flow tables, hazards, interlocks, models, mutual exclusion, operating system, program correctness, systems analysis.; Circuit analysis; Circuit synthesis; Delay effects; Delay lines; Hardware; Hazards; Input variables; Operating systems; Software systems; Sufficient conditions; Determinancy, flow tables, hazards, interlocks, models, mutual exclusion, operating system, program correctness, systems analysis.;
