Formalizing and validating properties in Asmeta with Large Language Models (Extended Abstract)
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910054769229824 |
|---|---|
| author | Bombarda, Andrea Bonfanti, Silvia Gargantini, Angelo Pellegrinelli, Nico |
| author_facet | Bombarda, Andrea Bonfanti, Silvia Gargantini, Angelo Pellegrinelli, Nico |
| contents | Writing temporal logic properties is often a challenging task for users of model-based development frameworks, particularly when translating informal requirements into formal specifications. In this paper, we explore the idea of integrating Large Language Models (LLMs) into the Asmeta framework to assist users during the definition, formalization, explanation, and validation of temporal properties. We present a workflow in which an LLM-based agent supports these activities by leveraging the Asmeta specification and the feedback produced by the model checker. This work serves as a proof of concept that illustrates the feasibility and potential benefits of such an integration through representative examples. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_15375 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Formalizing and validating properties in Asmeta with Large Language Models (Extended Abstract) Bombarda, Andrea Bonfanti, Silvia Gargantini, Angelo Pellegrinelli, Nico Software Engineering Writing temporal logic properties is often a challenging task for users of model-based development frameworks, particularly when translating informal requirements into formal specifications. In this paper, we explore the idea of integrating Large Language Models (LLMs) into the Asmeta framework to assist users during the definition, formalization, explanation, and validation of temporal properties. We present a workflow in which an LLM-based agent supports these activities by leveraging the Asmeta specification and the feedback produced by the model checker. This work serves as a proof of concept that illustrates the feasibility and potential benefits of such an integration through representative examples. |
| title | Formalizing and validating properties in Asmeta with Large Language Models (Extended Abstract) |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2603.15375 |