Simulation and Regression Testing Technique for Software Formal Specifications Based on Extended Place/Transition Net with Attributed Tokens

Authors
Tomohiko Takagi1, *, Ryo Kurozumi2
1Department of Engineering and Design, Faculty of Engineering and Design, Kagawa University, 2217-20 Hayashi-cho, Takamatsu-shi, Kagawa 761-0396, Japan
2Division of Reliability-based Information Systems Engineering, Graduate School of Engineering, Kagawa University, 2217-20 Hayashi-cho, Takamatsu-shi, Kagawa 761-0396, Japan
*Corresponding author. Email: [email protected]
Corresponding Author
Tomohiko Takagi
Received 25 November 2020, Accepted 11 May 2021, Available Online 21 July 2021.
DOI
https://doi.org/10.2991/jrnal.k.210713.009How to use a DOI?
Keywords
Formal specifications; place/transition net; VDM; simulation; regression testing
Abstract
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 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. 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.
Copyright
© 2021 The Authors. Published by ALife Robotics Corp. Ltd
Open Access
This is an open access article distributed under the CC BY-NC 4.0 license (http://creativecommons.org/licenses/by-nc/4.0/).