Title :
Using Pairwise Testing to Verify Automatically-Generated Formal Specifications
Author :
Salamah, Salamah ; Ochoa, Omar ; Jacquez, Yadira
Author_Institution :
Comput. Sci. Dept., Univ. of Texas at El Paso, El Paso, TX, USA
Abstract :
In this paper, we report on the effectiveness of the testing approach known as pairwise or orthogonal testing in verifying the correctness of the LTL specifications generated by the PROperty SPECification (Prospec) tool. This tool assists the user in generating a large number (over 34,000) of formal specifications in formal languages, including Linear Temporal Logic (LTL). Pairwise testing is a technique that aims at, significantly, reducing the amount of test cases required for testing a particular software system while providing assurance of adequate coverage of the problem space.
Keywords :
formal languages; formal specification; program testing; program verification; temporal logic; LTL specifications; Prospec tool; automatically-generated formal specification verification; formal languages; linear temporal logic; orthogonal testing; pairwise testing; property specification tool; software system testing; Formal specifications; Formal verification; Model checking; Runtime; Software systems; Composite Propositions; Formal specifications; LTL; Pairwise Testing; Pattern; Scope;
Conference_Titel :
High Assurance Systems Engineering (HASE), 2015 IEEE 16th International Symposium on
Conference_Location :
Daytona Beach Shores, FL
Print_ISBN :
978-1-4799-8110-6
DOI :
10.1109/HASE.2015.46
