We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.SE

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Software Engineering

Title: A systematic literature review on counterexample explanation

Abstract: Context: Safety is of paramount importance for cyber-physical systems in domains such as automotive, robotics, and avionics. Formal methods such as model checking are one way to ensure the safety of cyber-physical systems. However, adoption of formal methods in industry is hindered by usability issues, particularly the difficulty of understanding model checking results. Objective: We want to provide an overview of the state of the art for counterexample explanation by investigating the contexts, techniques, and evaluation of research approaches in this field. This overview shall provide an understanding of current and guide future research. Method: To provide this overview, we conducted a systematic literature review. The survey comprises 116 publications that address counterexample explanations for model checking. Results: Most primary studies provide counterexample explanations graphically or as traces, minimize counterexamples to reduce complexity, localize errors in the models expressed in the input formats of model checkers, support linear temporal logic or computation tree logic specifications, and use model checkers of the Symbolic Model Verifier family. Several studies evaluate their approaches in safety-critical domains with industrial applications. Conclusion: We notably see a lack of research on counterexample explanation that targets probabilistic and real-time systems, leverages the explanations to domain-specific models, and evaluates approaches in user studies. We conclude by discussing the adequacy of different types of explanations for users with varying domain and formal methods expertise, showing the need to support laypersons in understanding model checking results to increase adoption of formal methods in industry.
Comments: Accepted Manuscript. Information and Software Technology
Subjects: Software Engineering (cs.SE)
Journal reference: Information and Software Technology, Volume 145, December 2021, 106800
DOI: 10.1016/j.infsof.2021.106800
Cite as: arXiv:2201.03061 [cs.SE]
  (or arXiv:2201.03061v1 [cs.SE] for this version)

Submission history

From: Arut Prakash Kaleeswaran [view email]
[v1] Sun, 9 Jan 2022 17:46:34 GMT (807kb,D)

Link back to: arXiv, form interface, contact.