出版社：Information and Media Technologies Editorial Board
摘要：Formal methods are mathematically-based techniques for specifying, developing and verifying a component or system for increasing the confidence regarding the reliability and robustness of the target. It 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 code with conventional programming languages. For this purpose, millions of tests may be conducted in developing highly reliable mission-critical software in a lightweight formal approach. In this paper, we introduce our approach to supporting a large volume of testing for executable formal specifications using Hadoop, an implementation of the MapReduce programming model. We are able to automatically distribute an interpretation of specifications in VDM languages by using Hadoop. We also apply a property-based data-driven testing tool, QuickCheck, over MapReduce so that specifications can be checked with thousands of tests that would be infeasible to write by hand, often uncovering subtle corner cases that wouldn't be found otherwise. We observed effect to coverage and evaluated scalability in testing large amounts of data for executable specifications in our approaches.
