Time-Optimal Real-Time Test Case Generation Using Prioritized Time Petri Nets

This paper discusses the application of model checking to test generation from specifications written in prioritized time Petri nets. We demonstrate how to automatically generate conformance test cases, specially timed test cases with optimal execution time, using the model checker selt and the path analysis tool plan of the TINA toolbox.Properties are described in the SE-LTL temporal logic. Test cases are generated using manually formulated test purposes or automatically from various coverage criteria of the model.