An expressive and enriched specification language to synthesize behavior in BIG DATA systems

Abstract

In this work we extend our behavioral specification and controller synthesis framework FVS to deal with BIG DATA requirements. For one side, we enriched FVS expressive power by exhibiting how our language can handle fluents and partial specifications. For the other side, we combined FVS with a parallel model checker in order to automatically obtain a controller given the behavior specification. In this way, FVS can be presented as an attractive tool to formally verify and synthesize behavior for BIG DATA systems. Our approach is compared to other well known parallel tool analyzing a complex big data system.