Abstract:

High level Petri nets have been extensively used for system 
modeling; however their strong expressive power cost their 
analyzability. Currently, there are no effective general formal 
analysis techniques for high level Petri nets.  Fortunately, 
high level Petri nets are executable and as a result they can 
be tested. In recent years, some theoretical testing adequacy 
coverage measurements have been proposed. In this paper, we 
propose an approach to validate the above theoretical results 
through experiments using the simulation functionality of the 
model checker Spin.