Title :
Automated Testing of LTL Formula Generation by Prospec
Author :
Munoz, Cuauhtemoc ; Roach, Steve
Author_Institution :
Univ. of Texas at El Paso, El Paso, TX, USA
Abstract :
The Prospec software tool facilitates the construction of formal specifications in LTL by automating Dwyer´s Specification Pattern System as extended by Mondragon and Salamah. The LTL generation has been verified through the automated creation of a rigorous test set. Over 3 million test cases were generated and executed, providing extensive coverage of the system.
Keywords :
automatic testing; formal specification; program testing; program verification; software tools; Dwyer Specification Pattern System; LTL formula generation; LTL generation verification; Prospec software tool; automated testing; formal specification; test case generation; Classification algorithms; Generators; Software engineering; Software systems; Testing; USA Councils; LTL; Prospec; Specification Pattern System; automated testing;
Conference_Titel :
High-Assurance Systems Engineering (HASE), 2010 IEEE 12th International Symposium on
Conference_Location :
San Jose, CA
Print_ISBN :
978-1-4244-9091-2
Electronic_ISBN :
1530-2059
DOI :
10.1109/HASE.2010.31
