MC-FLoc: Learning from Traces to Locate Fault in Petri Net Model Checking

Model checking can automatically verify behavioral properties like deadlock-absence and linear temporal logic (LTL) specifications against a design model. When a model violates a property, a model checker can provide counterexamples. How-ever, it requires a lot of effort to identify the root cause. Model fault localization is widely recognized to be an expensive activity. What information in the counterexample can be used, and how to use this information to locate the root cause is still an open issue. We are the first to investigate the learning-based fault localization problem in model checking and propose an approach to locating the root cause in Petri net violating deadlock or LTL properties, called MC-FLoc. MC-FLoc learns fault location from the traces in the state graph of counterexamples. We present effective searching strategies to select faulty and correct traces and design a trace sorting algorithm so that similar traces are gathered to effectively learn the relationship between the nearby units. We construct five learning models and evaluate MC- Floc on a set of cases. The evaluation results show an average EXAM score of less than 13% on the deadlock benchmark and an average EXAM score of less than 20% on the LTL benchmark. This work is useful to practitioners of model checkers for providing a fault localization approach as well as establishing a benchmark for faulty software models. Our prototype and benchmark are publicly available at: https://github.com/MC-Floc/Floc.git.