Reference:
, "Combining Formal Verification and Testing for Correct Legacy Component Integration in Mechatronic UML", in Architecting Dependable Systems V, vol. 5135 of Lecture Notes in Computer Science, pp. 248–272, Springer Verlag, 2008.
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).
Links:
@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},
PDF = {uploads/pdf/GHH08_simulation_verification.pdf},
OPTacc_pdf = {},
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).}
}Copyright notice: This material is presented to ensure timely dissemination of
scholarly and technical work. Copyright and all rights therein are retained by
authors or by other copyright holders. All persons copying this information are
expected to adhere to the terms and constraints invoked by each author's copyright.
In most cases, these works may not be reposted without the explicit permission of
the copyright holder.
Powered by
bibtexbrowser