Model-based Testing and Analysis of Coordinated Components

Software components are common in the open source community. These components can be specified in model languages like AsmL or JML by using contracts (preconditions, postconditions). Starting from an integrated specification (components, coordinating process, wrapper), a model program is defined and used to define the formal semantics of the whole system. The relationship between coordinator and components are expressed as abisimulation. The model program can be used for conformance testing and generating test case suites when working with closed systems, and for scenario-based testing when working with reactive systems