Deriving State-Based Implementations of Interactive Components with History Abstractions

摘要

The external behaviour of an interactive component refers to the communication histories on the input and output channels. The component's implementation employs an internal state where inputs effect output and an update of the state. The black-box view is modelled by a stream processing function from input to output streams, the glass-box view by a state transition machine. We present a formal method how to implement a stream processing function with several arguments by a state transition machine in a correctness preserving way. The transformation involves two important steps, called differentiation and history abstraction. The differentiation localizes the effect of a single input on one of the input channels wrt. The previous input histories. The history abstraction introduces states as congruence classes of input histories. We extend our previous results from interactive components with one input channel to components with several input channels. The generalization employs a 'diamond property' for states and outputs which ensures the confluence of the resulting state transition system.