Model Checking for Input/Output Properties of a Black-Box Model

W. Dosch (Germany), P. Muenchaisri (Thailand), W. Ruanthong (Germany, Thailand), and A. Stümpel (Germany)


Stream processing, model checking, input/output be haviour, canonical Moore state transition machine, in put/output transition system, history abstraction.


The early phases of component-based software design fo cus 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 per formed on a state-transition model. This paper proposes a new approach how to model check input/output prop erties 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 be haviour. Model checking of input/output properties can be performed on the constructed input/output transition sys tem 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.

Important Links:

Go Back