Abstract :
Based on a program-proving technique, a method for proving sequential machine designs is presented. The method associates with each state of the machine an assertion about the sequences taking the machine into that state. The design is proved by: showing all assertions true irrespective of state changes; and deriving the design specifications from the assertions at final states. The method is illustrated´ on two finite automata.
Keywords :
Checking experiments, fault detection, finite automata, method of assertions, program proving, proof of designs, sequential machine design, switching theory.; Automata; Computer errors; Debugging; Error correction; Fault detection; Flowcharts; Logic design; Logic programming; Logic testing; Uncertainty; Checking experiments, fault detection, finite automata, method of assertions, program proving, proof of designs, sequential machine design, switching theory.;
