A methodology for evaluating test coverage criteria of high levelPetri nets

High level Petri nets have been extensively used for modeling concurrent systems; however, their strong expressive power reduces their ability to be easily analyzed. Currently there are few effective formal analysis techniques to support the validation of high level Petri nets. The executable nature of high level Petri nets means that during validation they can be analyzed using test criteria defined on the net model. Recently, theoretical test adequacy coverage criteria for concurrent systems using high level Petri nets have been proposed. However, determining the applicability of these test adequacy criteria has not yet been undertaken. In this paper, we present an approach for evaluating the proposed test adequacy criteria for high level Petri nets through experimentation. In our experiments we use the simulation functionality of the model checker SPIN to analyze various test coverage criteria on high level Petri nets.