Test case automation for specification patterns system and composite propositions.

摘要

Specifying software properties is a common activity in the software development process. Software properties are often written in a natural language such as English. However, the ambiguity in natural languages makes validation and verification time-consuming and error-prone. Specifying software properties in formal languages such as Linear Temporal Logic (LTL) or Computation Tree Logic (CTL) enables the use of formal verification tools such as model checkers. Nevertheless, formal languages require software developers to have a strong background in mathematics and logic.;The specification Patterns System (SPS) and Composite Propositions (CPs) use a higher-level abstraction to specify software properties formally. The SPS and CPs abstractions map to well-defined LTL formulas. These templates allow software developers to focus on the specification of software properties and not on the LTL formulas. Prospec is a software tool that uses SPS and CPs to specify software properties via a graphical user interface (GUI). The output of Prospec is an LTL formula that is derived from the corresponding specification. The algorithm for creating LTL formulas from SPS and CPs is complex, and this LTL generation must be verified. In this thesis work, a new algorithm to verify LTL formulas generated by Prospec is described. The algorithm was implemented and used to test Prospec's LTL generation by covering each of the combinations of patterns, scopes, and CPs. Results of this testing effort are discussed.