A Sound and Correct Formalism to Specify, Verify and Synthesize Behavior in BIG DATA Systems
A Sound and Correct Formalism to Specify, Verify and Synthesize Behavior in BIG DATA Systems
| dc.contributor.author | Asteasuain, Fernando | |
| dc.contributor.author | Rodriguez Caldeira, Luciana | |
| dc.date.accessioned | 2026-07-16T20:48:44Z | |
| dc.date.available | 2026-07-16T20:48:44Z | |
| dc.date.issued | 2022-5-20 | |
| dc.description.abstract | In this work we consolidate our behavioral specification frame work based on the Feather Weight Visual Scenarios (FVS) language as a powerful tool to specify, verify and synthesize behavior for BIG DATA systems. We formally demonstrate that our approach is sound and cor rect end to end, including the latest extensions such as fluents and par tial specifications. In addition, our empirical validation is strengthen by adding new and complex case studies and incorporating, besides execu tion time, space exploration as a factor in the comparison with other approaches. We believe that the contributions introduced in this work aim to point up FVS as a solid tool to formally verify behavior in BIG DATA systems. | |
| dc.identifier.citation | Asteasuain, F. & Caldeira, L.R. (2022). A Sound and Correct Formalism to Specify, Verify and Synthesize Behavior in BIG DATA Systems. In: Pesado, P., Gil, G. (eds) Computer Science – CACIC 2021. CACIC 2021. Communications in Computer and Information Science, vol 1584. Springer, Cham. | |
| dc.identifier.other | https://doi.org/10.1007/978-3-031-05903-2_8 | |
| dc.identifier.uri | https://repositorio.uai.edu.ar/handle/123456789/4994 | |
| dc.language.iso | en | |
| dc.publisher | Springer | |
| dc.subject | formal verification | |
| dc.subject | BIG DATA | |
| dc.subject | soundness | |
| dc.subject | correctness | |
| dc.title | A Sound and Correct Formalism to Specify, Verify and Synthesize Behavior in BIG DATA Systems | |
| dc.type | ARTICULO |