SUGISAKAMASANORI

Journal of Advances in Artificial Life Robotics
Vol. 4(3); December (2023), pp. 172–176
ON LINE ISSN 2435-8061; ISSN-L 2435-8061
https://alife-robotics.org/jallr.html

Research Article

Extending BWDM to Support Various Types and Recursive
Definitions in VDM++ Test Case Generation
Shota Takakura1, Tetsuro Katayama1, Yoshihiro Kita2, Hisaaki Yamaba1, Kentaro Aburada1, Naonobu Okazaki1

Department of Computer Science and Systems Engineering, Faculty of Engineering, University of Miyazaki, 1-1 Gakuen-kibanadai nishi, Miyazaki, 889-2192
Japan2
Department of Information Security, Faculty of Information Systems, Siebold Campus, University of Nagasaki, 1-1-1 Manabino, Nagayo-cho, Nishi-Sonogigun, Nagasaki, 851-2195 Japan
1ARTICLE INFO
Article History
Received 24 November 2023
Accepted 28 June 2024
Keywords
Software testing
Formal methods
VDM++
Automatic generation
Test cases

ABSTRACT

Generating test cases from VDM++ formal specifications, which help to eliminate ambiguities, isboth time-consuming and labor-intensive. To solve this problem, our laboratory has developed
BWDM, a tool for automatic test case generation from VDM++ specifications. However, theoriginal BWDM only supports integer types and cannot handle test cases for operations andfunctions with recursive structures. To enhance BWDM's usefulness, this paper introduces
extensions to address these limitations. The results confirm that the extended BWDM can reduce
test case generation time compared to manual methods.

© 2022 The Author. Published by Sugisaka Masanori at ALife Robotics Corporation Ltd.
This is an open access article distributed under the CC BY-NC 4.0 license(http://creativecommons.org/licenses/by-nc/4.0/)/.

only integer types and cannot handle test case generationfor operations and functions with recursive structures.
To enhance the functionality of BWDM, we haveintroduced the following extensions: A feature to generate test cases for enumeratedtypes
 A feature to generate test cases for operations andfunctions with recursive structures
This paper is organized as follows. Section 2 details theextended BWDM, Section 3 presents application
examples, and Section 4 discusses and validates theeffectiveness of BWDM. Finally, Section 5 concludes thepaper.

1. Introduction
Software plays an important to role support our daily
lives. Hence, its size and complexity have increased,leading to a greater societal impact of software bugs. One
significant cause of these bugs is the use of natural
language during the early stages of software development,
as natural language is inherently ambiguous. To solve
this problem, formal methods are adopted in software
design. Among these methods, VDM is widely used, andVDM++ serves as a formal specification language forobject-oriented modeling within VDM [1].
However, designing software with VDM++ necessitates
thorough testing. Manually generating test cases fromVDM++ specifications is both time-consuming andlabor-intensive, and it may result in incomplete testing.
To solve these problems, our laboratory has developed
BWDM [2], [3], an automated tool for generating test
cases from VDM++ specifications. Despite its usefulness,the current version of BWDM is limited to supporting

2. The Extended BWDMThis chapter describes on the enhancements in BWDM.
Fig. 1 illustrates the structure of the extended BWDM.

Corresponding author’s E-mail: kat@cs.miyazaki-u.ac.jp, takakura@earth.cs.miyazaki-u.ac.jp, kita@sun.ac.jp, yamaba@cs.miyazaki-u.ac.jp,
aburada@cs.miyazaki-u.ac.jp, oka@cs.miyazaki-u.ac.jp172

Fig. 1. The structure of the extended BWDM
Function Name : judgeLightColor
Argument Type : color:
Return Type : seq of (char)Class judgeLightColorTypes
public TrafficLight = <BLUE> | <YELLOW> | <RED>;functionsjudgeLightColor: TrafficLight ==> seq of charjudgeLightCoulor (color) ==if color = <BLUE >"The color is blue. "if color = <YELLOW>"The color is yellow"
if color = <RED>"The color is red."

Test Cases by Symbolic Execution
No.1 : <BLUE> -> "The color is blue"
No.2 : <YELLOW> -> "The color is yellow"
No.3 : <RED> -> "The clolor is red"Fig. 3. Output when Fig.4 is applied tothe extended BWDM
generation of input data for enumerated types throughsymbolic execution.

end judgeLightColor

Fig. 2. VDM++ specification using enumerated type2.2. Enhancing Test Case Generation for
Recursive Operations/Functions

2.1. Enhancing Test Case Generation for
Enumerated Types
To address the limitation of the original BWDM, which
only supported specific types, we enhance both theSyntax Analyzer and Symbolic Executor. Specifically,BWDM is extended to generate test cases for enumerated
types, which consist of a set of unique identifiers.
In the updated Syntax Analyzer, if an enumerated typedefinition is detected during the abstract syntax tree
analysis, the type declaration is replaced with a list
containing the declared name and values. When this list
is found in the syntax tree within the Symbolic Executor,
JavaAPI [4] is used to generate enumerated types,
creating constraints for the SMT solver [5] used in thepropositional analyzer section. This process enables the173

To address the limitation of the original BWDM ingenerating test cases for operations and functions withrecursive structures, we enhance both the Syntax
Analyzer and Test Suite Generator.
In the original BWDM, test cases could not be generated
if the parsing of a called operation/function wasincomplete during test suite generation. This issue
prevented the generation of an abstract syntax tree for
operations/functions with recursive calls.
To resolve this, we introduce an upper limit on thenumber of recursive calls for operations or functions with
self-recursive calls. The abstract parse tree analysis
process is modified to be executed after the parse tree
analysis for all definitions is completed. This ensures thattest data generation occurs only after the complete
parsing of the VDM++ specification. Additionally, afunction is added to terminate the process if self-recursive

Table 1. Comparison of test case generation time

Class ｓumOfNaturalNumbers
calcSum: nat ==> nat
factorial (value) ==if value = 0 then0else value + calcSum (value - 1)

In Fig. 4, the "calcSum" function is defined with arecursive structure. Fig. 5 confirms that test cases can begenerated for this recursive definition.

end sumOfNaturalNumbers

4. Discussion

Fig. 4. VDM++ specification with recursive structure

4.1. Verification of Test Case Generation for
Enumerated Types

Function Name : ｓumOfNaturalNumbers
Argument Type : value:nat
Return Type : nat

As discussed in Section 3.1, the extended BWDM
successfully generates test cases from definitions using
enumerated types in the VDM++ specification shown inFig. 2. This confirms that the extension allows BWDM tohandle enumerated type definitions, thereby enhancing
its usefulness.

Boundary Values for Each Argument
value: 4294967295 4294967294 0 -1
Test Cases of Boundary Values
No.1 : 4294967295 -> Undefined Action
No.2 : 4294967294 -> Undefined Action
No.3 : 0 -> 0No.4 : -1 -> Undefined Action

4.2. Evaluation of Test Case Generation for Recursive
Definitions
As detailed in Section 3.2, the extended BWDM iscapable of generating test cases from definitions withrecursive structures in the VDM++ specification shownin Fig. 4. This demonstrates that the extension enables
BWDM to manage recursive definitions, thus improving
its effectiveness.

Fig. 5. Output when Fig.6 is applied tothe extended BWDM
calls exceed the set limit during the output data
generation phase in the Test Suite Generator.
3. Application Examples

4.3. Comparison of Test Case Generation Time with
Manual Effort

This chapter presents examples to verify the functionalityof the extended BWDM.

We evaluate the time required to generate test cases using
the extended BWDM for VDM++ specifications that
include enumerated types and recursive structures,comparing it to manual efforts. The VDM++
specifications in Fig. 2 and Fig. 4 are used for thisexperiment. Manual verification is conducted by fivestudents: two graduate students and three fourth-year
undergraduates from our laboratory. The time taken togenerate comprehensive test cases without omissions isrecorded. The process is halted once the correct test cases
are produced, and any errors in the manually generated
test cases are noted. The comparison results are presented
in Table 1.
Table 1 indicates that using the extended BWDM saves
approximately 14 minutes compared to manual test casegeneration. Additionally, human errors have been
observed in the manual process. This study has confirmedthat the extended BWDM, which includes functions forgenerating test cases for enumerated types and recursivestructures, reduces both the time and errors associated3.1. Verification of Test Case Generation forEnumerated Types
Fig. 2 illustrates a VDM++ specification that use anenumerated type for verification purposes, and Fig. 3
displays the results obtained using the extended BWDM.
In Fig. 2, the "judgeLightColor" function defines "public
TraficLight = <BLUE>|<YELLOW>|<RED>;" as thetype. Fig. 3 demonstrates that test cases can be
successfully generated for this enumerated typedefinition.
3.2. Verification of Test Case Generation for
Recursive Definitions
Fig. 4 shows a VDM++ specification with a recursive
structure used for verification, and Fig. 5 shows thecorresponding results using the extended BWDM.
174

The application examples of the enhanced BWDM werepresented, demonstrating its ability to generate test cases
for definitions using enumerated types and recursivestructures, thereby broadening the range of supported
types. It has been confirmed that the extended BWDM
reduces test case generation time by approximately 14
minutes compared to manual methods. Additionally, theextended BWDM effectively eliminates human errors.
Consequently, the enhancements described in this paper
improve the usefulness of BWDM.
Future work includes: Extending support to types beyond integers andenumerated types
 Generating test cases for input values with a higher
number of recursive calls Generating test cases for mutually recursivefunctionswith manual test case generation. Therefore, theextension of BWDM enhances its usefulness.
4.4. Related Works
Ahmad Mustafa et al. conducted a systematic literature
review on automatic test case generation fromrequirement specifications [6]. They identified anddiscussed 30 primary studies out of 410, highlighting thatmost software testing errors from issues in natural
language requirements. Detecting ambiguities andincompleteness in natural language is challenging andremains an important problem in requirements.
On the other hand, BWDM uses the formal specification
language VDM++ for test case generation, producing test
cases from rigorous specifications that eliminate theambiguities and incompleteness. Therefore, BWDM does
not face the issues in test case generation fromrequirement specifications discussed in [6].
Some approaches to test case generation use UML as theinput [7], [8]. However, it is not possible to capture all
the different characteristics of a system from UML.
In contrast, BWDM uses the formal specification
language VDM++ for test case generation. Hence, it ispossible to capture all the different characteristics of asystem from a detailed VDM++ specification.
Aamer Nadeem et al. proposed a method for automatic
test case generation for VDM++ specifications [9]. Thismethod determines input data using pre-conditions andinvariant conditions described in the instance variable
definition block. These conditions are equivalence
partitioned, and a representative value is randomly
selected from the valid input domain. Additionally, a test
sequence is generated using a manually prepared test
descriptor defined as a valid test sequence. The input data
and test sequences are then combined to generate testcases.
In contrast, BWDM can generate test cases solely froma VDM++ specification. Furthermore, test cases
generated by BWDM can be used for boundary value
testing and domain analysis testing. Test cases generated
through symbolic execution can also cover execution
flows that boundary value analysis might miss.

References
1.
2.

3.

4.

5.
6.

7.

8.

5. Conclusion

9.

To enhance the usefulness of BWDM, an automatic test
case generation tool for VDM++ specifications, twoimportant extensions have been implemented. These
extensions address the limitations of supporting only
integer types, and the inability to generate test cases for
operations and functions with recursive structures.
175

OvertureProject.
Manuals.
https://www.overturetool.org/documentation/manuals.ht
ml. (Accessed: 2023-12-18).
T. Katayama, F. Hirakoba, Y. Kita, H. Yamaba, K.
Aburada, and N. Okazaki. Application of Pirwise Tsting
into BWDM which is a Test Case Generation tool for theVDM++ Specification. Journal of Robotics, Networkingand Artificial Life, Vol.6, No.3, pp.143-147, 2019.
T. Muto, T. Katayama, Y. Kita, H. Yamaba, K. Aburada,and N. Okazaki. Expansion of Application Scope andAddition of a Function for Operations into BWDM which
is an Automatic Test C55-262, 2022.
Z3 Prover/z3. htt ases Generation Tool for VDM++
Specification. Journal of Robotics, Networking andArtificial, Vol.9. No.3, pp.2ps://github.com/Z3Prover/z3.
(Accessed: 2024-6-27).
Z3:
Packagecom.microsoft.z3.
https://z3prover.github.io/api/html/namespacecom_1_1
microsoft_1_1z3.html. (Accessed: 2024-6-27).
Ahmad Mustafa, Wan M. N. Wan-Kadir, Noraini Ibrahim,Muhammad Arif Shah. Automated Test Case Generationfrom Requirements: A Systematic Literature Review.
Computers, Materials & Continua, vol. 67, no.2, pp.
1819-1833, 2021.
M. Lafi, T. Alrawashed, A. M. Hammad. Automated TestCases Generation From Requirements Specification,
International Conference on Information Technology(ICIT), pp. 852-857, 2021.
Mauricio Rocha, Adenilso Simão, Thiago Sousa. Modelbased test case generation from UML sequence diagramsusing extended finite state machines. Software Quality
Journal, Volume 29, Issue 3, pp.597-627, 2021.
Aamer Nadeem, Muhammad Jaffar-Ur-Rehman.
Automated Test Case Generation from IFAD VDM++
Specifications. SEPADS 05: 4th WSEAS International
Conference on Software Engineering, Parallel &Distributed Systems, No.28, pp.1-7, 2005.

Dr. Naonobu Okazaki
He received his B.S, M.S., and Ph.D.
degrees in electrical and communicationengineering from Tohoku University,
Japan, in 1986, 1988 and 1992,
respectively. He joined the Information
Technology Research and Development
Center, Mitsubishi Electric Corporation in1991. He is currently a Professor with theFaculty of Engineering, University of Miyazaki since 2002.
His research interests include mobile network and network
security. He is a member of IPSJ, IEICE and IEEE.

Authors Introduction
Mr. Shota Takakura
He received the Bachelor's degree inengineering (computer science andsystemsengineering)from
theUniversity of Miyazaki, Japan in 2023.
He is currently a Master's student in
Graduate School of Engineering at theUniversity of Miyazaki, Japan. His
research interests include software
testing, software quality, and formal method.
Dr. Tetsuro Katayama
He received a Ph.D. degree in engineeringfrom Kyushu University, Fukuoka, Japan,in 1996. From 1996 to 2000, he has beena Research Associate at the Graduate
School of Information Science, Nara
Institute of Science and Technology,
Japan. Since 2000 he has been an
Associate Professor at the Faculty ofEngineering, Miyazaki University, Japan. He is currently aProfessor with the Faculty of Engineering, University ofMiyazaki, Japan. His research interests include software
testing and quality. He is a member of the IPSJ, IEICE, andJSSST.
Dr. Yoshihiro Kita
He received a Ph.D. degree in systems
engineering from the University ofMiyazaki, Japan, in 2011. He is currentlyan Associate Professor with the Faculty ofInformation Systems, University ofNagasaki, Japan. His research interests
include software testing and biometricsauthentication.
Dr. Hisaaki Yamaba
He received the B.S. and M.S. degrees inchemical engineering from the Tokyo
Institute of Technology, Japan, in 1988
and 1990, respectively, and the Ph D.
degree in systems engineering from theUniversity of Miyazaki, Japan in 2011. He
is currently an Assistant Professor with theFaculty of Engineering, University ofMiyazaki, Japan. His research interests include network
security and user authentication. He is a member of SICE
and SCEJ.
Dr. Kentaro Aburada
He received the B.S., M.S, and Ph.D.
degrees in computer science and systemengineering from the University ofMiyazaki, Japan, in 2003, 2005, and 2009,
respectively. He is currently an Associate
Professor with the Faculty of Engineering,
University of Miyazaki, Japan. His
research interests include computer networks and security.
He is a member of IPSJ and IEICE.

176