From Stream Transformers to Moore State Transition Machines with Input and Output

摘要

A black box specification of a deterministic software or hardware component refers to the function mapping input histories to output histories. An important refinement step amounts to designing a state transition machine which correctly implements the specified behaviour. We present a formal method for implementing stream transformers by Moore state transition machines. First we construct a canonical Moore state transition machine whose state space is based on input histories. Then we identify output equivalent states for achieving a reduced Moore state transition machine. We illustrate the formal method with various applications.