Title :
Time-Optimal Real-Time Test Case Generation Using Prioritized Time Petri Nets
Author :
Adjir, Noureddine ; de Saqui-Sannes, P. ; Rahmouni, Mustapha Kamel
Author_Institution :
ISAE, Univ. of Toulouse, Toulouse, France
Abstract :
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.
Keywords :
Petri nets; formal specification; program testing; temporal logic; SE-LTL temporal logic; TINA toolbox; model checking; path analysis tool plan; prioritized time Petri nets; time-optimal real-time test case generation; Automata; Automatic testing; Life testing; Logic; Parallel processing; Petri nets; Power system modeling; Processor scheduling; Real time systems; System testing; Prioritzed Time petri Nets; real-time system;
Conference_Titel :
Advances in System Testing and Validation Lifecycle, 2009. VALID '09. First International Conference on
Conference_Location :
Porto
Print_ISBN :
978-1-4244-4862-3
Electronic_ISBN :
978-0-7695-3774-0
DOI :
10.1109/VALID.2009.31
