Automatic generation and verification of complex pattern-based software specifications.

摘要

Verifying software correctness is a fundamental part of the software production process. Software verification techniques include testing and formal verification. Formal verification techniques, such as theorem proving, runtime-monitoring, and model checking are based on formal specifications of software behavior, which require expert knowledge of formal languages to read, write, and validate. This is one reason why software developers have not widely adopted formal verification techniques. There have been successful research efforts to minimize the challenges of using formal specifications including the Specification Pattern System (SPS), and Composite Propositions (CPs). SPS uses a series of templates of commonly used software specifications to provide practitioners a system for specifying software without being experts in formal languages. Prospec is a software tool designed to visually guide practitioners during the specification of software behavior using SPS properties and CPs, which are abstractions that describe the relationship between two or more propositions.; A recent research effort into generating Linear Temporal Logic (LTL) formulas from SPS resulted in a set of LTL specification templates that support CPs. The specifications generated by instantiating templates with the existing CP classes need to be verified and validated to ensure that they maintain the original semantics of the SPS patterns and scopes. This thesis focuses on the problem of testing specification templates. In this work, we introduce model checker-based testing, a general method for testing software specifications based on SPS patterns and composite propositions. This method can be used to test templates not only in LTL but in different formalisms such as Computational Tree Logic (CTL) and Graphical Interval Logic (GIL).; In order to validate the testing method, this work introduces the Property Testing Framework (PROTEF), a software framework to automatically generate and test formulas representing software specifications, in particular, specifications based on SPS and composite propositions. As a case study, we tested a subset of the LTL templates. The result of a case study provides evidence that our testing method is feasible and effective.