Timed k-Tail: Automatic Inference of Timed Automata

TL;DR

Timed k-Tail is a novel technique for automatically inferring timed automata from program traces, capturing both functional and timing behaviors to improve system analysis and anomaly detection.

Contribution

It introduces Timed k-Tail, the first method to mine timed automata from traces, integrating timing information into specification mining.

Findings

Efficiently mines accurate timed automata models

Effectively identifies anomalous timing executions

Produces few false positives in anomaly detection

Abstract

Accurate and up-to-date models describing the be- havior of software systems are seldom available in practice. To address this issue, software engineers may use specification mining techniques, which can automatically derive models that capture the behavior of the system under analysis. So far, most specification mining techniques focused on the functional behavior of the systems, with specific emphasis on models that represent the ordering of operations, such as tempo- ral rules and finite state models. Although useful, these models are inherently partial. For instance, they miss the timing behavior, which is extremely relevant for many classes of systems and com- ponents, such as shared libraries and user-driven applications. Mining specifications that include both the functional and the timing aspects can improve the applicability of many testing and analysis solutions. This paper addresses this challenge by presenting the Timed k-Tail (TkT) specification mining technique that can mine timed automata from program traces. Since timed automata can effectively represent the interplay between the functional and the timing behavior of a system, TkT could be exploited in those contexts where time-related information is relevant. Our empirical evaluation shows that TkT can efficiently and effectively mine accurate models. The mined models have been used to identify executions with anomalous timing. The evaluation shows that most of the anomalous executions have been correctly identified while producing few false positives.

Full text

See pages 1-last of paper.pdf