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.