@InCollection{GHH08,
  AUTHOR = {Giese, Holger and Henkler, Stefan and Hirsch, Martin},
  TITLE = {{Combining Formal Verification and Testing for Correct Legacy
  Component Integration in Mechatronic UML}},
  YEAR = {2008},
  BOOKTITLE = {Architecting Dependable Systems V},
  VOLUME = {5135},
  PAGES = {248--272},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer Verlag},
  URL = {http://dx.doi.org/10.1007/978-3-540-85571-2_11},
  ABSTRACT = {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 sucha
  composition means for a sufficient verification either by testing or
  formal verification are necessary. However, the overwhelmingcomplexity
  of the interaction of distributed real-time components usually excludes
  that testing alone can provide the requiredcoverage 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 architecturalmodel. This is in the subsequent steps enriched by
  an incremental synthesis using formal verification techniques for the
  systematicgeneration 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 couldnot be covered by
  testing, local testing of the components guided by the verification
  results is employed to derive refinedbehavioral models. The approach
  further has two outstanding benefits. It can pin-point real failures
  without false negativesright 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).}
}