DocumentCode
3060482
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
fYear
2010
fDate
3-4 Nov. 2010
Firstpage
168
Lastpage
169
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;
fLanguage
English
Publisher
ieee
Conference_Titel
High-Assurance Systems Engineering (HASE), 2010 IEEE 12th International Symposium on
Conference_Location
San Jose, CA
ISSN
1530-2059
Print_ISBN
978-1-4244-9091-2
Electronic_ISBN
1530-2059
Type
conf
DOI
10.1109/HASE.2010.31
Filename
5634288
Link To Document