Research on the interactive property testing based on Petri net

The aim of property based testing is to validate an IUT with respect to a target property, to observe whether the property is violated or not. Many distributed systems have a natural feature-Interactive property. But most distributed systems face state explosion when the test work is analyzed and developed with a formal model. In order to avoid such problems, this paper presents a testing method that is Interactive property based testing, which can focus on the interesting features of a system. Petri net is employed to model the IUT, so we can make use of its reachability graph to generate the executable test sequence. Furthermore a test sequence generation algorithm is proposed and analyzed. We also give a verdict method. The feasibility of the approach is illustrated on a BRP case study.