Dynamic property mining for embedded software

The importance of specification definition in the embedded software design flow has been proven over the years. The entire design process relies on the specification quality, which inevitably depends on designer knowledge and skills. Automatic property mining is part of the efforts proposed to make this activity easier for the designers. Nonetheless, the existing approaches are limited to the detection of either arithmetic invariants of programs or temporal properties for Boolean designs, e.g., bit-level hardware descriptions. In this work, we present a dynamic mining approach able to infer linear temporal logic (LTL) properties for embedded software. The mined properties are in the form of temporal relationships between arithmetic expressions. The approach considers the execution traces only, thus it is completely independent from the code implementation. Experimental results demonstrate the effectiveness of the approach