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.

 

@inproceedings{MoreiraC:2024b,
 author = {E. Moreira and J.C. Campos},
 title = {A language for explaining counterexamples},
 booktitle = {13th Symposium on Languages, Applications and Technologies (SLATE 2024)},
 year = {2024},
 series = {OpenAccess Series in Informatics (OASIcs)},
 volume = {120},
 pages = {11:1-11:14},
 publisher = {Schloss Dagstuhl - LZI},
 doi = {10.4230/OASIcs.SLATE.2024.11},
 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.}
}

Generated by mkBiblio 2.6.28