DROPS

Document

DOI: 10.4230/OASIcs.SLATE.2024.11

A Language for Explaining Counterexamples

Authors: Ezequiel José Veloso Ferreira Moreira and José Creissac Campos

Published in: OASIcs, Volume 120, 13th Symposium on Languages, Applications and Technologies (SLATE 2024)

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

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)

Copy BibTex To Clipboard

@InProceedings{velosoferreiramoreira_et_al:OASIcs.SLATE.2024.11,
  author =	{Veloso Ferreira Moreira, Ezequiel Jos\'{e} and Campos, Jos\'{e} Creissac},
  title =	{{A Language for Explaining Counterexamples}},
  booktitle =	{13th Symposium on Languages, Applications and Technologies (SLATE 2024)},
  pages =	{11:1--11:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-321-8},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{120},
  editor =	{Rodrigues, M\'{a}rio and Leal, Jos\'{e} Paulo and Portela, Filipe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2024.11},
  URN =		{urn:nbn:de:0030-drops-220826},
  doi =		{10.4230/OASIcs.SLATE.2024.11},
  annote =	{Keywords: Model Checking, NuSMV, counterexample, natural language explanation}
}

Search Results

Documents authored by Campos, José Creissac

A Language for Explaining Counterexamples

Abstract

Cite as

Thanks for your feedback!

Could not send message