More Testable Properties

The journal paper More Testable Properties has been recently accepted for publication in the journal Software Tools for Technology Transfer.

This paper is joint work with my friends and colleagues from Verimag (Jean-Claude Fernandez and Laurent Mounier) and from Inria Rennes – Bretagne Atlantique (Thierry Jéron and Hervé Marchand).

The paper shall appear in STTT shortly. One can download a preprint of the paper meanwhile.

Below is an abstract of the paper:

In this article, we explore the set of testable properties within the Safety-Progress classification where testability means to establish by testing that a relation, between the tested system and the property under scrutiny, holds. We characterize testable properties w.r.t. several relations of interest. For each relation, we give a sufficient condition for a property to be testable. Then, we study and delineate a fine-grain characterization of testable properties: for each Safety-Progress class, we identify the subset of testable properties and their corresponding test oracle. Furthermore, we address automatic test generation for the proposed framework by providing a general synthesis technique that allows to obtain canonical testers for the testable properties in the Safety-Progress classification. Moreover, we show how the usual notion of quiescence can be taken into account in our general framework, and, how quiescence improves the testability results. Then, we list some existing testing approaches that could benefit from this work by addressing a wider set of properties. Finally, we propose Java-PT, a prototype Java toolbox that implements the results introduced in this article.