Abstract
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.
Original language | English |
---|---|
Pages | 120-127 |
Number of pages | 8 |
Publication status | Published - 01.12.2007 |
Event | 3rd IASTED International Conference on Advances in Computer Science and Technology - Phuket, Thailand Duration: 02.04.2007 → 04.04.2007 Conference number: 74017 |
Conference
Conference | 3rd IASTED International Conference on Advances in Computer Science and Technology |
---|---|
Abbreviated title | ACST 2007 |
Country/Territory | Thailand |
City | Phuket |
Period | 02.04.07 → 04.04.07 |