Mining Temporal Properties of Data Invariants
Caroline Lemieux · 2015
System specifications are important in maintaining program correctness, detecting bugs, understanding systems and guiding test case generation. Often, these specifications are not explicitly written by developers. If we want to use them for analysis, we need to obtain them through other methods; for example, by mining them out of program behavior. Several tools exist to mine data invariants and temporal properties from program traces, but few examine the temporal relationships between data invariants. An example of this kind of relationship would be "the return value of the method isFull? is false until the field size reaches the value capacity". We propose a data-temporal property miner, Quarry, which mines Linear Temporal Logic (LTL) relations of arbitrary length and complexity between Daikon-style data invariants. We infer data invariants from systems using Daikon, recompose these data invariants into sequences, and mine temporal properties over these sequences. Our preliminary results suggest that this method may recover important system properties.