Expansion of Application Scope and Addition of a Function for Operations into BWDM which is an Automatic Test Cases Generation Tool for VDM++ Specification

The use of the formal specification description language VDM++ in software design can eliminate ambiguity in the specification. However, software testing after implementation is necessary even if the design uses VDM++, but manually generating test cases is labor-intensive and timeconsuming. Therefore, our laboratory developed BWDM, which is an automatic test case generation tool for VDM++ specifications. However, BWDM is not very useful because it has three problems about its narrow scope of application. This paper solves the three problems and improves the usefulness of BWDM by expanding the scope of application of VDM++ definitions and adding a function to generate test cases for object states. In addition, we conducted a comparison experiment with manual test case generation and confirmed that BWDM can reduce work time.