Model checking for input/output properties of a black-box model

The early phases of component-based software design focus on the interaction between the components and the environment. Each component is considered as a black box whose input/output behaviour is described by a stream transformer mapping input histories to output histories. Model checking is an automatic verification approach performed on a state-transition model. This paper proposes a new approach how to model check input/output properties of a component's black box model. To this end, we systematically construct an input/output state transition system which reflects the component's input/output behaviour. Model checking of input/output properties can be performed on the constructed input/output transition system in a sound way. The overall transformation from the stream transformer to the transition system uses canonical Moore machines as an intermediate artifact. We illustrate the approach with a simple example and discuss possible extensions.