Document Open Access Logo

A Language for Explaining Counterexamples

Authors Ezequiel José Veloso Ferreira Moreira , José Creissac Campos

PDF

File

Thumbnail PDF
PDF
OASIcs.SLATE.2024.11.pdf
  • Filesize: 0.68 MB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Model Checking
  • NuSMV
  • counterexample
  • natural language explanation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Model checkers can automatically verify a system’s behavior against temporal logic properties. However, analyzing the counterexamples produced in case of failure is still a manual process that requires both technical and domain knowledge. However, this step is crucial to understand the flaws of the system being verified. This paper presents a language created to support the generation of natural language explanations of counterexamples produced by a model checker. The language supports querying the properties and counterexamples to generate the explanations. The paper explains the language components and how they can be used to produce explanations.

Cite As Get BibTex

Ezequiel José Veloso Ferreira Moreira and José Creissac Campos. A Language for Explaining Counterexamples. In 13th Symposium on Languages, Applications and Technologies (SLATE 2024). Open Access Series in Informatics (OASIcs), Volume 120, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/OASIcs.SLATE.2024.11

Author Details

Ezequiel José Veloso Ferreira Moreira
  • Universidade do Minho, Braga, Portugal
  • INESC TEC, Braga, Portugal
José Creissac Campos
  • Universidade do Minho, Braga, Portugal
  • INESC TEC, Braga, Portugal

Funding

  • Veloso Ferreira Moreira, Ezequiel José: acknowledges FCT (Fundação para a Ciência e Tecnologia) grant 2023.01639.BD, funded by the ESF (European Social Fund) and PQDI (Programa Demografia, Qualificações e Inclusão).

References

  1. John J. Camilleri, Mohammad Reza Haghshenas, and Gerardo Schneider. A web-based tool for analysing normative documents in english. In Proceedings of the 33rd Annual ACM Symposium on Applied Computing, SAC '18, pages 1865-1872, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3167132.3167331.
  2. J. C. Campos and M. D. Harrison. Interaction engineering using the ivy tool. In ACM Symposium on Engineering Interactive Computing Systems (EICS 2009), pages 35-44, New York, NY, USA, 2009. ACM. URL: https://doi.org/10.1145/1570433.1570442.
  3. Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Nusmv 2: An opensource tool for symbolic model checking. In Computer Aided Verification, pages 359-364, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-45657-0_29.
  4. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, April 1986. URL: https://doi.org/10.1145/5397.5399.
  5. Edmund M Clarke. The birth of model checking. In Orna Grumberg and Helmut Veith, editors, 25 Years of Model Checking, volume 5000 of Lecture Notes in Computer Science, pages 1-26. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-69850-0_1.
  6. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, Cambridge, MA, USA, 1999. Google Scholar
  7. Andrew Crapo, Abha Moitra, Craig McMillan, and Daniel Russell. Requirements capture and analysis in assert(tm). In 2017 IEEE 25th International Requirements Engineering Conference (RE), pages 283-291, 2017. URL: https://doi.org/10.1109/RE.2017.54.
  8. M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In Proc. 21st International Conference on Software Engineering, ICSE '99, pages 411-420. ACM, 1999. URL: https://doi.org/10.1145/302405.302672.
  9. Lu Feng, Mahsa Ghasemi, Kai-Wei Chang, and Ufuk Topcu. Counterexamples for robotic planning explained in structured language. In 2018 IEEE International Conference on Robotics and Automation (ICRA), pages 7292-7297. IEEE, 2018. URL: https://doi.org/10.1109/ICRA.2018.8460945.
  10. M.D. Harrison, P. Masci, and J.C. Campos. Verification templates for the analysis of user interface software design. IEEE Transactions on Software Engineering, 45(8):802-822, August 2019. URL: https://doi.org/10.1109/TSE.2018.2804939.
  11. Anne Elisabeth Haxthausen. An Introduction to Formal Methods for the Development of Safety-critical Applications. DTU Orbit, 2010. Google Scholar
  12. Arut Prakash Kaleeswaran, Arne Nordmann, Thomas Vogel, and Lars Grunske. A systematic literature review on counterexample explanation. Information and Software Technology, 145:106800, 2022. URL: https://doi.org/10.1016/j.infsof.2021.106800.
  13. Lionel van den Berg, Paul Strooper, and Wendy Johnston. An automated approach for the interpretation of counter-examples. Electronic Notes in Theoretical Computer Science, 174(4):19-35, 2007. Proceedings of the Workshop on Verification and Debugging (V&D 2006). URL: https://doi.org/10.1016/j.entcs.2006.12.027.
  14. Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald. Formal methods: Practice and experience. ACM Comput. Surv., 41(4), October 2009. URL: https://doi.org/10.1145/1592434.1592436.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact