Mining signal temporal logic specifications for hybrid systems

Several approaches have been proposed over the years to automatically generate specifications of digital systems by means of dynamic techniques, which are now ripe to be applied in large-scale industrial scenarios. On the other hand, the automatic extraction of specifications for the hybrid domain, where systems express both discrete and continuous behaviours, remains mainly unexplored. Therefore, in this paper, we propose a tool for dynamically mining the specifications of hybrid systems in the form of assertions compliant with the Signal Temporal Logic (STL), which has been proven to be effective at capturing the behaviours of such systems. Our approach takes as input a set of execution traces of the target system and mixes clustering and decision-tree algorithms to generate STL assertions that describe what has been actually implemented.