Journal of Robotics, Networking and Artificial Life, Vol. 4, No. 2 (September 2017) 110–113___________________________________________________________________________________________________________BWDM: Test Cases Automatic Generation Tool
Based on Boundary Value Analysis with VDM++*

Tetsuro Katayama*, Hiroki Tachiyama*, Yoshihiro Kita†,
Hisaaki Yamaba*, Kentaro Aburada*, and Naonobu Okazaki*

University of Miyazaki, 1-1 Gakuen-kibanadai nishi, Miyazaki, 889-2192 Japan†Tokyo University of Technology, 1404-1 Katakura, Hachioji, 192-0914 Japan
E-mail: kat@cs.miyazaki-u.ac.jp, tachiyama@earth.cs.miyazaki-u.ac.jp,
kitayshr@stf.teu.ac.jp, yamaba@cs.miyazaki-u.ac.jp, aburada@cs.miyazaki-u.ac.jp, oka@cs.miyazaki-u.ac.jp

Abstract
For software development using Formal Methods, we have developed a prototype of the boundary value test caseautomatic generation tool BWDM. The main two topics of our tool are (1) automatically generation of test casesand (2) boundary value analysis. Our tool improves the efficiency of software testing process in using VDM++ thatis one of the Formal Methods. In this research, we show the composition of our tool, application example,
evaluation of the usefulness, relative research, and future issues.
Keywords: Software Testing, Boundary Value Analysis, Formal Methods, VDM++

1. Introduction

On the other hand, either way designed using natural
languages or formal specification languages, it needs
software testing after implementation of software. In
order to test software, it is necessary to design test cases,
but it takes much time and effort to design them
manually. Therefore, by efficiently designing test cases,
it is possible to improve the efficiency of the testingprocess. It is also important to design test cases focusedon places where bugs can be hidden, in order to improvethe efficiency of executing of software testing.
Therefore, in this research, we develop a prototypeof test case automatic generation tool BWDM
(Boundary Value/Vienna Development Method) for the
purpose of improving the efficiency of the test process
in software development using formal methods. We use
Boundary Value Analysis1 for test cases designing. We
use the “boundary value test case” what means the test
case designed based on boundary value analysis.

A cause of coming into bugs in software is using natural
languages in process of software design. Naturallanguages are ambiguous. And this causes
misunderstanding of developers in designing documents.
Finally, they implement software based on themisunderstanding, and the software will have bugs.
As one method to solve this problem, FormalMethods are suggested that used in upstream process ofsoftware development. In developing process of using
formal methods, specification is described whatcharacteristic of development target, by using notnatural languages but formal specification languages
what based on mathematical logic. For that reason,
unlike conventional development, specification can beproved its correctness of description contents byarithmetical theorem proofs, mechanical inspection, etc.
In other words, it is possible to write strict specification
document which is excluded ambiguous description.

Copyright © 2017, the Authors. Published by Atlantis Press.
This is an open access article under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).
110

Journal of Robotics, Networking and Artificial Life, Vol. 4, No. 2 (September 2017) 110–113___________________________________________________________________________________________________________Fig. 1. The flow of BWDM processing

Fig. 3. The flow of expected output data generator processing

written in the VDM++ specification. And it outputs test
cases that consists of input data and expected outputdata.
3. Application Example
Fig. 2. The flow of input data generator processing

2. Boundary Value Test
Generation Tool BWDM

Case

We apply the formal specification that mixed inequality
expression and surplus expression to BWDM. And wecheck 3 items.

Automatic(i) BWDM is operated correctly.
(ii) The boundary value is correctly extracted from theVDM++ specification.
(iii) BWDM outputs the input data and the expected
output data correctly as the boundary value testcase.

BWDM analyzes boundary values of function
definitions that described in VDM++ specification, andautomatically generates boundary value test cases.
Figure 1 shows the flow of BWDM processing. Notethat VDM is a formal method devised at the IBM
Vienna Research Institute in the 1970s, and VDM++ isan object-oriented extension of VDM-SL2 which isformal specification language of VDM.
BWDM consists of input data generator andexpected output data generator. In process of expectedoutput data generator, the decision table is used, what isgenerated by decision table generation support tool
developed in our laboratory3. The inputs into BWDM
are VDM++ specification and decision table. Here, we
implement BWDM in Java language.

Figure 4 shows formal specification that we applyto BWDM. This specification judges whether the firstargument is even or odd, and whether the second
argument is a positive number or a negative number.
Figure 5 shows the generated test cases by applying theformal specification of Figure 4 to BWDM.
The boundary values generated from the argument
arg1 of the specification in Fig. 4 are natMin-1, natMin,natMax, natMax+1, 1, 2, and 3. And from the argument
arg2, intMin-1, intMin, intMax, intMax+1, -1, and 0 aregenerated. Here, “natMin-1” means a value which is one
less than the minimum value of the natural type.
BWDM generates all combinations of boundary valuesof each of the two variables as input data. Therefore, thenumber of test cases generated from this specification is7 * 6 = 42 (cases). By Fig. 5, we can check test cases
from No. 1 to No. 42. From this, it is clear that BWDM
outputs correct test cases from the formal specification.
Also, we can check that both of extracting boundary
values from VDM++ specification and outputtingboundary value test cases that consist both of input dataand expected output data are correct as well.

2.1. Process of input data generator
Figure 2 shows the flow of processing of input data
generator. The input is VDM++ specification file. And
this unit generates input data based on boundary valueanalysis.
2.2. Process of expected output generator
Figure 3 shows the flow of processing of expected
output data generator. This unit generates expected
output data when input data is input to a function that is111

Journal of Robotics, Networking and Artificial Life, Vol. 4, No. 2 (September 2017) 110–113___________________________________________________________________________________________________________Fig. 4. The formal specification that mixed inequality
expression and surplus expression

4. Discussion
In this research, for the purpose of improving theefficiency of the test process in software developmentusing formal methods, we have developed a prototypeof boundary value test case automatic generation tool
BWDM. The inputs to BWDM are VDM++
specification and decision table, and the test caseautomatic generation and the boundary value analysis tothe function definition in the specification areperformed. Therefore, this tool improves the efficiency
both of designing of test case and conducting of testing.
In the followings, we consider BWDM.

Fig. 5. The test cases generated by applying the formal
specification of Figure 4 to BWDM

4.1. Evaluation of usefulness

seconds. The number of rules on the decision table for
specification 1 (number of columns in the decisiontable) is 32, specification 2 is 1024 and specification 3
is 1048576. These represent the number of states thatthe function can take, depending on the Boolean value
in the if-conditional expression. When constraint
conditions such as preconditions are described in thespecification, the number of states actually taken by thefunction is less than this number. However, it istroublesome and time consuming to manually design
test cases for functions that can have as many states aspossible. On the other hand, BWDM can automaticallygenerate boundary value test cases in several seconds if
the specification is up to condition number 15.
Hence, we think that BWDM is usefulness when
testing software that implemented from VDM++
specification.

To consider BWDM usefulness, we used 3specifications. We measured the time to generate testcases. Table 1 shows conclusion of measuring. Within
the three specification, the if-conditional expressions ofinequalities are described. The specification 1 has 5 ifconditional expressions, specification 2 has 10expressions and specification 3 has 15 expressions. To
measure execution time, we used System.nanoTime4
method of Java. We measured the time that is to give
the VDM++ specification and the decision table as an
input to the BWDM and to finish outputting the testcases. The unit of time was millisecond, andmeasurements were made five times for eachspecification, and we calculated the average of 5
measuring as well. Here, we don’t consider the time toprepare the VDM++ specification and the decision table.
For the average time in each specification,
specification 1 and specification 2 were less than 0.5
seconds, and specification 3 was less than seven112

Journal of Robotics, Networking and Artificial Life, Vol. 4, No. 2 (September 2017) 110–113___________________________________________________________________________________________________________

productivity and quality of developed software isexpected.
Future works are as follows.
•
Generation of boundary values not appearing inthe specification description
Although it does not appear as a concrete
numerical value in the specification description,
there are boundary values that occur when twoor more if-conditional expressions are related,
and the current BWDM cannot generate thosevalues as input data. It is necessary to modify
the current process to generate boundary values.
•Responding to various environments
Current BWDM, boundary value analysis ofargument types of function definition cannot
cope with various environments (bit numberand development language) used for actualdevelopment. It is necessary to implement afunction to allow users to set information about
test cases what they want.

Table 1. Generation time of test cases fromthree specifications
Times

Specification1 Specification2 Specification3

1st time
2nd time
3rd time
4th time
5th time
Average

325
283
500
291
269
334

316
389
371
334
371
356

6277
5321
6236
5070
5700
5720

4.2. Related research
TOBIAS5 is a test cases automatic generation tool for
testing theVDM++
specification.
TOBIAS
automatically generates test cases according to a test
pattern input to TOBIAS. It is defined by test designerusing a regular expression to output a test case.
Both TOBIAS and BWDM support the testing
phase of software development using VDM++.
TOBIAS supports testing the VDM++ specification. In
contract, BWMD supports testing actually implementedsoftware.
This is what the difference of between two tools.
Therefore, when you need to test implemented software,
BWDM is superior.

Acknowledgements
This work was supported by JSPS KAKENHI Grant
Number 24220001.

5. Conclusion

References

In this research, we have developed a prototype of test
cases automatic generation tool BWDM based onboundary value analysis targeting the VDM++
specification with the aim of streamlining the testingprocess in software development using formal method.
We applied the VDM++ specification that mixed
inequality expression and surplus expression into
BWDM, and our tool analyzed boundary value of thespecification correctly. Finally, BWDM outputs test
cases that consist both of input data and expected output
data correctly. Furthermore, as a result of applying threekinds of VDM++ specifications including up to 15 ifconditional expressions to BWDM, it generated test
cases within about seven seconds. Therefore, BWDM
improves the efficiency of designing test cases.
In conclusion, by using BWDM, it is expected to
improve the efficiency of the test process in softwaredevelopment using formal methods. Moreover, byconducting test design and test process based on theVDM++ specification, improvement both of1. Blake
Neate,
Boundary
value
analysis,
http://www.cs.swan.ac.uk/~csmarkus/CS339/docs.htm,(accessed June 26, 2017).
2. International Organization for Standardization, ISO/IEC
JTC
1/SC
22/WG,
Information
technology-Programming languages, their environments and system
software interfaces--Vienna Development Method-Specification Language--Part 1: Base language (1996)
3. Kenta Nishikawa, Tetsuro Katayama, Yoshihiro Kita,
Hisaaki Yamaba and Naonobu Okazaki, Proposal of a
Supporting Method to Generate a Decision Table fromthe Formal Specification, International Conference on
Artificial Life and Robotics, 222-225 (2014)
4. Java System class,https://docs.oracle.com/javase/jp/6/api/java/lang/System.
html, (accessed June 26, 2017).
5. Olivier Maury, Yves Ledru, Pierre Bountron and Lydie
du Bousquet, Using TOBIAS for the automatic generation of VDM test cases, http://vasco.imag.fr/Tobias/Papers/vdm02tobias.pdf, (accessed June 26, 2017).

113