RT Book, Section
T1 Formal correctness of a passive testing approach for timed systems
A1 García Merayo, María De Las Mercedes
A1 Andrés Sánchez, César
A1 Núñez García, Manuel
AB In this paper we extend our previous work on passivetesting of timed systems to establish a formal criterion to determine correctness of an implementation under test. In our framework, an invariant expresses the fact that if the implementation under test performs a given sequence of actions, then it must exhibit a behavior in a lapse of time reflected in the invariant. In a previous paper we gave an algorithm to establish the correctness of an invariant with respect to a specification. In this paper we continue the work by providing an algorithm to check the correctness of a log, recorded form the implementation under test, with respect to an invariant. We show the soundness of our method by relating it to an implementation relation. In addition to the theoretical framework we have developed a tool, called PASTE, that facilitates the automation of our passive testing approach.
PB IEEE Comp Soc
SN 978-0-7695-3671-2
YR 2009
FD 2009-04
LK https://hdl.handle.net/20.500.14352/45319
UL https://hdl.handle.net/20.500.14352/45319
LA eng
NO International Conference on Software Testing, Verification, and Validation Workshops. APR 01-04, 2009. Denver, CO.
NO MEC
DS Docta Complutense
RD 10 abr 2025