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
