Formally Verifying Data Science Systems with a Sound and Correct Formalism

Abstract

The state explosion problem arises as one of the most problematic issues to be faced against when trying to formally validate Data Science Software Systems. This challenge imposes the synergy and combination of tools. Taking this into consideration in this work we present a robust theoretical feature of our behavioral framework VG-FVS: we formally prove that our approach relies on a sound, complete and correct formalism. VG-FVS is a brand new new version of our framework FVS (Feather weight Visual Scenarios), which is specially developed to address the state explosion problem by integrating FVS with MaRDiGraS, a generic library which eases the state space exploration using a MAP-REDUCE software architecture.