On Testing 1-Safe Petri Nets

Formal models are often considered for software systems specification, and are helpful for verifying that certain properties are respected, or for automatically generating the implementation code corresponding to the model, or again for conformance testing, for the automatic generation of test cases to check an implementation against the formal specification. Variations of finite state machine (FSM) models have been mostly used for conformance testing, while the otherwise very popular formal model of Petri nets is seldom mentioned in this context. In this paper, we look at the question of conformance testing when the model is provided in the form of a 1-safe Petri net. We provide a general framework for conformance testing, and give algorithms for deriving test cases under different assumptions: besides the adaptation of methods originally developed for FSMs which lead to exponentially long test sequences, we have identified cases for which polynomial testing algorithms for free-choice Petri nets can be provided. These results are significant when modeling concurrent systems, as exemplified by workflow modeling.