Abstract
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]