Visual counterexample explanation for model checking with Oeritte

TL;DR

Oeritte is a visual tool that helps users interpret model checking results by providing explanations and causality visualizations for counterexamples in function block diagrams, improving usability for complex systems.

Contribution

This paper introduces Oeritte, a novel visual explanation tool that enhances understanding of model checking counterexamples in industrial systems.

Findings

Oeritte effectively visualizes causality in counterexamples.

It reduces debugging efforts in formal verification.

The tool improves interpretability of model checking results.

Abstract

Despite being one of the most reliable approaches for ensuring system correctness, model checking requires auxiliary tools to fully avail. In this work, we tackle the issue of its results being hard to interpret and present Oeritte, a tool for automatic visual counterexample explanation for function block diagrams. To learn what went wrong, the user can inspect a parse tree of the violated LTL formula and a table view of a counterexample, where important variables are highlighted. Then, on the function block diagram of the system under verification, they can receive a visualization of causality relationships between the calculated values of interest and intermediate results or inputs of the function block diagram. Thus, Oeritte serves to decrease formal model and specification debugging efforts along with making model checking more utilizable for complex industrial systems.