hvc13 Arcaini, Paolo Gargantini, Angelo Riccobene, Elvinia

Online testing of LTL properties for Java code

in Hardware and Software: Verification and Testing, Haifa Verification Conference HVC 2013 (Eds. Bertacco, Valeria and Legay, Axel) Springer Berlin / Heidelberg, LNCS-Lecture Notes in Computer Science, vol. 8244 (2013): 95--111 ISBN 978-3-319-03076-0

LTL specifications are commonly used in runtime verification to describe the requirements about the system behavior. Efficient techniques derive, from LTL specifications, monitors that can check if system executions respect these properties. In this paper we present an \online testing approach which is based on LTL properties of Java programs. We present an algorithm able to derive and execute test cases from monitors for LTL specifications. Our technique actively tests a Java class, avoids false failures, and it is able to check the correctness of the outputs also in the presence of nondeterminism. We devise several coverage criteria and strategies for visiting the monitors, providing different qualities in terms of test size, testing time, and fault detection capability.

[read the copyright and download the pdf file] [DOI] [url]

My sw links