Takafumi Muto1, Tetsuro Katayama1, Yoshihiro Kita2, Hisaaki Yamaba1, Kentaro Aburada1, Naonobu Okazaki1
1Department of Computer Science and Systems Engineering, Faculty of Engineering,
University of Miyazaki, 1-1 Gakuen-kibanadai nishi, Miyazaki, 889-2192
Japan
2Department of Information Security, Faculty of Information Systems, Siebold
Campus, University of Nagasaki, 1-1-1 Manabino, Nagayo-cho, Nishi-Sonogi-gun,
Nagasaki, 851-2195 Japan
pp. 255–262
ABSTRACT
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 time-consuming.
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.
ARTICLE INFO
Article History
Received 25 November, 2021
Accepted 14 September 2022
Keywords
Software testing
Formal methods
Test cases
VDM++
Automatic generation.
JRNAL9308
Download article (PDF)