Test Cases Automatic Generation from VDM++

Go to Japanese Ver.

last updated 21/September 2017


BWDM image


In the upstream of software development, the ambiguity of natural languages (say, English, Japanese) becomes a problem for designing software.

The ambiguity of natural languages makes ambiguous specification.
Ambiguous specification causes ambiguous understanding of the system to be developed.
Implementation based on ambiguos understanding causes discrepancies between specification and implementation.
Finally, bugs are included in the software.

To solve this issue, Formal Methods are suggested.
By designing the software with formal specification language instead of natural languages,
it's available strict specification.
VDM (Vienna Development Method) is one of the formal methods. And VDM-SL is formal specification language of VDM.

In this research, to improve the efficiency of test designing in software development with formal methods,
we develop Test Cases Automatic Generation Tool:BWDM (Boundary Value/Vienna Development Method).
BWDM analyzes boundary values of software specification written in VDM++ that is object-oriented dialect of VDM-SL,
and generates test cases.

Input and Output

input and output image

Input and output are shown below.

The decision table is generated by the decision table generation support tool developed in this laboratory.
Input for this support tool is VDM++ specification, and its output is a decision table that format is csv (comma separated values).
And test cases generated by BWDM consist of input data and expected output data.

Function and Corresponding Syntax

Parsing : By using VDMJ (https://github.com/NickBattle).
Extraction : Extract information (argument types, parameter, if-conditions) from fucntion definition for boundary value analysis.
Boundary Value Analysis : Generate boundary values based on extracted information. And generate test cases.


Now, the constraction of VDM++ that BWDM can analyze is function definition only.
Also, BWDM can not analyze pre conditions and post conditions too.
The argument types are only Integer (int ,nat, nat1).
The number of arguments of function is only two.

Future Issues

future image

It has been found that there are cases where it isn't possible to cover all the paths by current analysis.
For this reasen, we implement processing based on Symbolic Execution.