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

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.