Reachability and Propagation for LTL Requirements Testing

It is important to test software with respect to user requirements, especially when adhering to safety standards, which require traceability from requirements to test cases. While research has resulted in many different model based testing techniques, only a few consider requirement properties; this paper helps fill this gap. We identify two fundamental characteristics of a test case intended to evaluate a given requirement property. The two characteristics are adapted from the venerable Reachability, Infection, and Propagation (RIP) model for faults and failures in ordinary code. In the context of requirements testing, we propose the reachability property amounts to the property not being vacuously true on a given test case, and the propagation property amounts to a potential violation of the property on the test case being observable. In particular, we formalize these notions in the context of requirement properties expressed in linear temporal logic (LTL), and not only show how to determine reachability and propagation for given test cases, but also how to modify test cases to satisfy these properties. To demonstrate the importance of reachability and propagation we evaluate test sets for a small real-life application generated according to previously published test criteria.