E. Moreira and J.C. Campos
Explaining temporal logic model checking counterexamples through the use of structured Natural Language
In Engineering Interactive Computer Systems, volume 14517 of Lecture Notes in Computer Science. 2024. (in press)

Abstract

The use of model checking tools allows for the formal verification of properties over models of systems, improving their robustness. However, these tools are challenging to use, and their results require much work of interpretation to communicate to stakeholders. To address this issue, the IVY Workbench offers a plethora of options to make the process of creating and understanding the models, properties and results of the verification process more accessible, with a particular focus on interactive computing systems. Despite this, there is still a significant requirement of expertise to use the tool. To solve this, an approach to provide structured natural language explanations for the results of model checking-based tools is being developed, to be later incorporated into the IVY Workbench. This paper presents the current state of the approach's development, stating its objective and what results can already be achieved.

@inproceedings{MoreiraC:2024,
 author = {E. Moreira and J.C. Campos},
 title = {Explaining temporal logic model checking counterexamples through the use of structured Natural Language},
 booktitle = {Engineering Interactive Computer Systems},
 year = {2024},
 series = {Lecture Notes in Computer Science},
 volume = {14517},
 note = {in press},
 abstract = {The use of model checking tools allows for the formal verification of properties over models of systems, improving their robustness. However, these tools are challenging to use, and their results require much work of interpretation to communicate to stakeholders. To address this issue, the IVY Workbench offers a plethora of options to make the process of creating and understanding the models, properties and results of the verification process more accessible, with a particular focus on interactive computing systems. Despite this, there is still a significant requirement of expertise to use the tool. To solve this, an approach to provide structured natural language explanations for the results of model checking-based tools is being developed, to be later incorporated into the IVY Workbench. This paper presents the current state of the approach's development, stating its objective and what results can already be achieved.}
 }

Generated by mkBiblio 2.6.26