Large Volume Testing for Executable Formal Specification Using Hadoop

Formal methods are mathematically-based techniques for specifying, developing and verifying a component or system, in order to increase the confidence regarding to the reliability and robustness of the target. Formal methods can be used at different levels with different techniques, and one approach is to use model-oriented formal languages such as VDM languages in writing specifications. During model development, we can test executable specifications in VDM-SL and VDM++. In a lightweight formal approach, we test formal specifications to increase our confidence as we do in implementing software codes with conventional programming languages. While the specific level of rigor depends on the aim of the project, millions of tests may be conducted in developing highly reliable mission-critical software in a light-weight formal approach. In this paper, we introduce our approach to supporting large volume of testing for executable formal specifications using Hadoop, an implementation of MapReduce programming model. We are able to automatically distribute interpretation of specifications in VDM languages by using Hadoop. We also apply a property-based data-driven testing tool, Quick Check, over MapReduce so that specification can be checked with thousands of tests by using formally described pre/post conditions and invariant functions. As an advanced property-based data-driven testing approach, we also discuss model-based testing. We observed scalable performance in testing large amount of data for executable specifications in our approaches.