Automated failure analysis in model checking based on data mining

This paper presents an automated failure analysis approach based on data mining. It aims to ease and accelerate the debugging work in formal verification based on model checking if a safety property is not satisfied. Inspired by the Kullback-Leibler Divergence theory and the TF-IDF (Term Frequency - Inverse Document Frequency) measure, we propose a suspiciousness factor to rank potentially faulty transitions on the error traces in time Petri net models. This approach is illustrated using a best case execution time property case study, and then further assessed for its efficiency and effectiveness on an automated deadlock property test bed.