Issue No.12 - December (1971 vol.20)
S.K. Abdali , IEEE
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.
Checking experiments, fault detection, finite automata, method of assertions, program proving, proof of designs, sequential machine design, switching theory.
S.K. Abdali, "On Proving Sequential Machine Designs", IEEE Transactions on Computers, vol.20, no. 12, pp. 1563-1566, December 1971, doi:10.1109/T-C.1971.223170