Journal of Robotics, Networking and Artificial Life
Vol. 8(2); September (2021), pp. 112–116
DOI: https://doi.org/10.2991/jrnal.k.210713.009; ISSN 2405-9021; eISSN 2352-6386
https://www.atlantis-press.com/journals/jrnal

Research Article

Simulation and Regression Testing Technique for Software
Formal Specifications Based on Extended Place/Transition
Net with Attributed Tokens
Tomohiko Takagi1,*, Ryo Kurozumi2
Department of Engineering and Design, Faculty of Engineering and Design, Kagawa University, 2217-20 Hayashi-cho, Takamatsu-shi,
Kagawa 761-0396, Japan
2
Division of Reliability-based Information Systems Engineering, Graduate School of Engineering, Kagawa University, 2217-20 Hayashi-cho,Takamatsu-shi, Kagawa 761-0396, Japan
1

ARTICLE INFOABSTRACT

Article History

We propose a technique of simulation and regression testing for Extended Place/transition Net with Attributed Tokens(EPNAT) models, and then show a prototype tool to partially support it. In the technique, the information about a current
marking, current values of variables, and current fireable transitions is indicated to assist engineers in finding faults andselecting next transitions to be fired for the simulation. Also, good execution traces in the simulation are recorded as test cases
for the regression testing. When an EPNAT model is modified, the test cases can be applied to it in order to reveal regression
failures. A preliminary experiment using simple software requirements has been carried out to discuss the effectiveness of the
proposed technique.

Received 25 November 2020
Accepted 11 May 2021
Keywords
Formal specifications
place/transition net
VDM
simulation
regression testing© 2021 The Authors. Published by Atlantis Press International B.V.
This is an open access article distributed under the CC BY-NC 4.0 license (http://creativecommons.org/licenses/by-nc/4.0/).

1. INTRODUCTION
Formal specifications that represent the way to realize software requirements in unambiguous and executable forms play
an important role in the development of high-quality software.
Extended Place/transition Net with Attributed Tokens (EPNAT)[1] is a formal specification description language for modelingthe expected behavior of state transition-based software that consists of multiple objects, such as modules and subsystems. In an
EPNAT model, each attributed token corresponds to an object andhas variables to characterize the object, which are called attributes.
The firing of transitions leads to the increase, decrease and moveof attributed tokens, the change of values of attributes and global
variables, and so on. The behavior is constrained by invariants,
pre-conditions, post-conditions, and type constraints, which arecollectively called constraints. Engineers need to understand suchcomplex aspects of the EPNAT model when constructing, validating and refining it. EPNAT is a new language, and thus systematic
techniques to address this problem need to be developed.
In this paper, we propose a technique of simulation and regression testing for EPNAT models, and then show a prototype tool
to partially support it. In the technique, the information about
a current marking (that is, a current distribution of attributed
tokens, including current values of attributes), current values ofglobal variables, and current fireable transitions is indicated toCorresponding author. Email: takagi@eng.kagawa-u.ac.jp*

assist engineers in finding faults and selecting next transitions to
be fired for the simulation. Also, good execution traces in the simulation are recorded as test cases for the regression testing. Whenan EPNAT model is modified, the test cases can be applied to it
to reveal regression failures. This technique has been developed
only for EPNAT. A preliminary experiment using simple software
requirements has been carried out to discuss the effectiveness of
our technique.
EPNAT models can be converted into VDM++ specifications thatcan be supported by existing tools [2]. They also enable engineers
to perform interactive execution and regression testing. The maindifferences between our technique and the existing tools are that(i) our technique focuses on more abstract aspects of software
specifications, (ii) our technique emphasizes the understandingof software specifications, and (iii) our technique cannot support
test-first [3].
This paper is organized as follows. Section 2 describes our technique of simulation and regression testing for EPNAT models, andthen Section 3 illustrates our prototype tool. Section 4 gives anexperimental result to discuss the effectiveness of our technique.
Finally, we show conclusion and future work in Section 5.

2. TECHNIQUE OVERVIEW
In this section, we propose the technique of simulation and regression testing for EPNAT models.

T. Takagi and R. Kurozumi / Journal of Robotics, Networking and Artificial Life 8(2) 112–116

2.1. Simulation of EPNAT Models
The simulation is intended to help engineers to construct, validate,refine, and understand EPNAT models, and it is applicable to bothcompleted EPNAT models and EPNAT models under construction. The simulation of a given EPNAT model is performed according to the following procedure. The overview of the procedure isshown in Figure 1. Step 2, 3, and 5 can be automatically executed,
and should be supported by a tool to save time and effort.
Step 1. An engineer specifies a starting state (that is, a state to start
the simulation) according to the aim of the simulation. In
this study, a state is characterized by a marking and valuesof all the global variables in an EPNAT model. Note that amarking in an EPNAT model includes values of attributes.
The starting state does not necessarily have to be an initialstate (that is, a state established just after software is invoked)
or reachable state (that is, a state that can be reached fromthe initial state).
Step 2. If the starting state violates any type constraints and invariants, this procedure returns to Step 1. Otherwise, the current state of the given EPNAT model is initialized to thestarting state.

113

Step 3. The pre-conditions of all the transitions are evaluated todetermine fireable transitions in the current state. If there
are no fireable transitions, the simulation is terminated.
Step 4. The engineer confirms the determined fireable transitions
and acceptable values of their arguments. If he/she finds any
faults, the simulation will be stopped. Otherwise, the engineer selects one arbitrary fireable transition and specifies
values of its arguments according to the aim of the simulation.
Step 5. If the specified values of the arguments violate any type
constraints, invariants and pre-condition, this procedure
returns to Step 4. Otherwise, the selected transition isfired, and then its actions are executed by using the specified values of arguments. As a result of them, the current
state is changed. If any invariants, and the post-condition of
the fired transition are violated due to some sort of failures
included in the given EPNAT model, the simulation will be
stopped.
Step 6. The engineer confirms the current state. If he/she finds any
faults, or if he/she achieves the aim of the simulation, thesimulation will be terminated. Otherwise, this procedure
returns to Step 3.

2.2. Regression Testing of EPNAT Models
A good execution trace in the simulation is recorded as a test casefor the regression testing of future EPNAT models. In this context, the word “good” means that (a) the execution trace does notinclude the occurrence of faults, (b) the execution trace accelerates
the growth of test coverage, (c) the execution trace corresponds tothe typical use of software, and (d) the execution trace is useful tocover fault-prone parts [4]. The item (a) is particularly essential fora test case.
When an EPNAT model is modified, the test cases are applied to it
to reveal regression failures. Some model-based coverage criteria[5,6] can be introduced to evaluate the effectiveness of the regression testing. Additionally, EPNAT models can be converted into
VDM++ specifications [1], and thus common code-based coverage
criteria [7] also can be introduced. In general, multiple test cases
need to be executed to satisfy a coverage criterion. Also, regression
testing is repeatedly performed, and thus it should be automated bya tool to save time and effort.

Figure 1 | Procedure of simulation (overview).

Figure 2 shows the abstracted structure of a test case for an EPNAT
model. It is written in BNF, and parentheses are used to represent an
optional element. A test case is a sequence of successive state transitions of arbitrary length. Each transition is identified by an event,and can have values of arguments. Each transition should follow
fireable transitions that include its event. Fireable transitions are
determined by a state, and thus should follow a state in a test case.
Each state is characterized by a marking and values of all the global
variables. If an invalid value is given to an argument of a transition
to test a constraint, the following state should be a violation state,that is, a state in which the constraint has been violated. A marking
is expressed as a sequence of attributed tokens in each place, andan attributed token is characterized by object type and values of
attributes. Each place can hold one or more attributed tokens, but

114

T. Takagi and R. Kurozumi / Journal of Robotics, Networking and Artificial Life 8(2) 112–116

the place and its attributed tokens need to have the same object
type. Therefore, the object type of each attributed token is important information in the regression testing of EPNAT models.
The flow of the regression testing is similar to the one of the simulation. A starting state and transitions correspond to test data (alsocalled test input), and are used in Step 1 and 4, respectively. On
the other hand, fireable transitions and states excepting the startingstate correspond to expected output, and are used in Step 4 and6, respectively. When there are no differences between expected
output and test output through the execution of a given test case, it
is concluded that the test case has successfully passed. Otherwise,
an engineer needs to find and fix a regression failure, or update
the test case so as to reflect the latest true software specification.
After that, the engineer should perform confirmation testing, that
is, apply the failed test case to the fixed EPNAT model, or apply the
updated test case to the EPNAT model.

An EPNAT model under simulation is visualized on the rightpane of (C). Fireable transitions in the current state are highlighted in green. Therefore, an engineer will be able to easily
confirm them, and select a next transition to proceed with his/her simulation. Also, the current state and the simplified execution trace (described as a sequence of fired transitions) areindicated on the left pane. When an engineer selects a fireable
transition and specifies its values of arguments on the right pane,(C) automatically executes the firing of the selected transition,
executes its actions, evaluates constraints, and then updates thecurrent state, the execution trace, and the graphical image of
the EPNAT model. An engineer can stop and reset the current
simulation at any time. When an engineer thinks that the execution trace is good for a test case in regression testing, he/she
can save it.
An engineer can start automated regression testing by loading a test
case and an EPNAT model to be tested.

3. PROTOTYPE TOOLThis section shows our prototype tool to partially support thesimulation and regression testing of EPNAT models. As shown in
Figure 3, the prototype tool consists of (A) EPNAT model editor,(B) VDM++ specification editor, and (C) EPNAT simulator. (A)and (B) have been developed in our previous study [1], and (C) has
been developed in this study. (A) allows an engineer not only toconstruct his/her EPNAT model using GUI, but also to automatically convert the model into a VDM++ specification. The VDM++
specification can be further developed by using (B). When an
EPNAT model on (A) needs to be simulated, (C) can be invokedfrom (A). (C) interacts with an existing tool called VDMJ [2] toexecute a given EPNAT model.

4. EXPERIMENT
To discuss the effectiveness of the proposed technique, we have carried out a preliminary experiment using software requirements of asimple load balancer [1]. In the experiment, the simulation on our
prototype tool is compared with Scenario-Based Reading (SBR),
that is, a review technique [8] to find faults in normal software
specifications by using expected usage scenarios. The experimentconsists of the following four steps:
Step 1. In accordance with the software requirements, we correctly
create software Specifications written in a Natural language(SN) and an EPNAT model.

Figure 2 | Abstracted structure of a test case for an EPNAT model (written in BNF).

A

B

C

Figure 3 | Screen shots of our prototype tool. (A) EPNAT model editor. (B) VDM++ specification editor. (C) EPNAT simulator.

T. Takagi and R. Kurozumi / Journal of Robotics, Networking and Artificial Life 8(2) 112–116

Table 1 | Experimental results
Technique
SBR
Simulation

Detection rate
f1

f2

f3

Ave.

1/5
4/5

2/5
4/5

0/5
1/5

0.2
0.6

Ave. no.
0.6
1.8

Step 2. We insert three faults f1, f2 and f3 into SN, and create Faulty
SN (FSN). Additionally, we insert the three faults into the
EPNAT model, and create a faulty EPNAT model.

115

transitions to be fired for the simulation. Also, good execution
traces in the simulation are recorded as test cases for the regression
testing. When an EPNAT model is modified, the test cases can beapplied to it to reveal regression failures. This technique has beendeveloped only for EPNAT. We have carried out a preliminary
experiment using simple software requirements. The results of theexperiment and of the interview indicate the effectiveness of thetechnique, but further evaluation will be needed in future study.

Step 3. In accordance with the software requirements, we correctly
create three expected usage scenarios s1, s2 and s3 for SN.
They are written in a natural language. s1 is useful to reveal
f2, and s3 is useful to reveal f1. Additionally, we convert thethree expected usage scenarios into three simplified execution traces for the EPNAT model.

When a failure that was caused in the earlier stage of softwaredevelopment is found in the later stage (typically, the processes ofsystem testing and acceptance testing), the cost to fix it generally
tends to become higher. Therefore, it is important to find and fix
failures in the earlier stage, and it is expected that our technique
can be applied to address this problem. However, our tool is underdevelopment, and the functions to support our technique are notcompletely implemented at present. Also, the following mattersneed to be tackled in future work in order to improve the technique:

Step 4. Five students (three in the master’s course and two in theundergraduate course at our university) read the software
requirements. After that, each of them performs SBR, thatis, tries to find the three faults in FSN by using the three
expected usage scenarios within 20 min. Additionally, eachof them performs the simulation, that is, tries to find thethree faults in the faulty EPNAT model by using the three
simplified execution traces within 20 min.

•• An engineer will often need to confirm that the set of reachable
states in an EPNAT model under construction includes all theindispensable states to satisfy given software requirements andalso the set does not include any invalid states. However, test
cases are manually created in our technique and tool, and thus itwill be difficult for most engineers to do such task systematicallyat small cost. Model checking [9] may be useful to address thisproblem.

Table 1 shows the results of this experiment. The simulation has
greater detection rate of each fault than SBR. The average numberof faults detection per one student is 1.8 on simulation, and is 0.6
on SBR. After the experiment, we interviewed each of the students
and got the following comments:•• After an engineer has made a modification on an EPNAT model,
he/she will often need to maintain some existing test cases, thatis, to update some existing test cases so as to reflect the latest true
software specification. A technique and tool to systematicallysupport it should be constructed.

•• The EPNAT model, rather than SN, was or might be useful tounderstand the software (three students).

•• Coverage criteria are useful to create good execution traces insimulation and to select good test cases in regression testing.
Engineers will need guidelines for the effective use of coverage
criteria, and will need a tool to automatically suggest execution
traces and test cases according to coverage criteria.

•• It was easier to find faults in the faulty EPNAT model than in
FSN (five students).
•• The simulation is useful for understanding the EPNAT model(four students). The simulation is useful for testing and validating, rather than for understanding (another student).
•• There is room to improve the user interface of the prototype
tool (two students).
The results of the experiment and of the interview indicate theeffectiveness of our technique. However, note that the simulation
follows SBR in Step 4, and thus the students may have developed
the understanding of the given faulty software specifications before
starting the simulation. Further evaluation will be needed in future
study.

5. CONCLUSION AND FUTURE WORKIn this paper, we have proposed a technique of simulation andregression testing for EPNAT models, and then have shown a prototype tool to partially support it. In the technique, the information
about a current marking (including current values of attributes),
current values of global variables, and current fireable transitions
is indicated to assist engineers in finding faults and selecting next

Based on the above, we will develop the tool to support our extended
technique, and apply it to pilot projects to evaluate its effectiveness.

CONFLICTS OF INTEREST
The authors declare they have no conflicts of interest.

ACKNOWLEDGMENT
This work was supported by JSPS KAKENHI Grant Number
JP17K00103.

REFERENCES[1]

T. Takagi, R. Kurozumi, Software modeling technique and its
prototype tool for behavior of multiple objects using extended
place/transition nets with attributed tokens, J. Robot. Netw. Artif.
Life 7 (2020), 194–198.

T. Takagi and R. Kurozumi / Journal of Robotics, Networking and Artificial Life 8(2) 112–116

116

[2]
[3]
[4]
[5]

J. Fitzgerald, P.G. Larsen, P. Mukherjee, N. Plat, M. Verhoef,
Validated designs for object-oriented systems, Springer-Verlag,
London, 2005.
K. Beck, Test-driven development: by example, Addison-Wesley
Professional, Boston, MA, United States, 2002.
J.A. Whittaker, J. Arbon, J. Carollo, How google tests software,
Addison-Wesley Professional, Boston, MA, United States, 2012.
T. Takagi, R. Kurozumi, T. Katayama, State transition tuple
coverage criterion for extended place/transition net-based testing, Proceedings of the 2019 IEEE Pacific Rim International
Symposium on Dependable Computing (PRDC), IEEE, Kyoto,
Japan, 2019, pp. 29–30.

[6]

[7]
[8]
[9]

T. Takagi, N. Oyaizu, Z. Furukawa, Concurrent N-switch coverage criterion for generating test cases from place/transition nets,
Proceedings of the 2010 IEEE/ACIS 9th International Conference
on Computer and Information Science, IEEE, Yamagata, Japan,
2010, pp. 782–787.
B. Beizer, Software testing techniques, 2nd ed., Van Nostrand
Reinhold, New York, NY, United States, 1990.
T. Thelin, P. Runeson, C. Wohlin, An experimental comparisonof usage-based and checklist-based reading, IEEE Trans. Softw.
Eng. 29 (2003), 687–704.
E.M. Clarke, O. Grumberg, D.A. Peled, Model checking, MIT
Press, Cambridge, MA, United States, 1999.

AUTHORS INTRODUCTION
Dr. Tomohiko Takagi
He received the B.S., M.S. and PhD
degrees from Kagawa University in 2002,
2004 and 2007, respectively. He becamean Assistant Professor in 2008, and a lecturer in 2013 in the Faculty of Engineeringat Kagawa University. Since 2018 he has
been an Associate Professor in the Facultyof Engineering and Design at Kagawa
University. His research interests are in software engineering,particularly software testing.

Mr. Ryo Kurozumi
He received the B.S. degree from Kagawa
University in 2019. He is a master’s student
in the Graduate School of Engineering at
Kagawa University. His research interests
are in software engineering, particularly
software design.