A Sound and Correct Formalism to Specify, Verify and Synthesize Behavior in BIG DATA Systems

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.