One of the main benefits of component-based architectures is their support for reuse. The port and interface definitions of
architectural components facilitate the construction of complex functionality by composition of existing components. For such
a composition means for a sufficient verification either by testing or formal verification are necessary. However, the overwhelming
complexity of the interaction of distributed real-time components usually excludes that testing alone can provide the required
coverage when integrating a legacy component. In this paper we present a scheme on how embedded legacy components can be tackled.
For the embedded legacy components initially a behavioral model is derived from the interface description of the architectural
model. This is in the subsequent steps enriched by an incremental synthesis using formal verification techniques for the systematic
generation of component tests. The proposed scheme results in an effective combination of testing and formal verification.
While verification is employed to tackle the inherently subtle interaction of the distributed real-time components which could
not be covered by testing, local testing of the components guided by the verification results is employed to derive refined
behavioral models. The approach further has two outstanding benefits. It can pin-point real failures without false negatives
right from the beginning. It can also prove the correctness of the integration without learning the whole legacy component
(using the restrictions of the integration context).
This work was developed in the course of the Special Research Initiative 614 - Self-optimizing Concepts and Structures in
Mechanical Engineering - University of Paderborn, and was published on its behalf and funded by the Deutsche Forschungsgemeinschaft.