Validated templates for specification of complex LTL formulas

Formal verification approaches that check software correctness against formal specifications have been shown to improve program dependability. Tools such as Specification Pattern System (SPS) and Property Specification (Prospec) support the generation of formal specifications. SPS has defined a set of patterns (common recurring properties) and scopes (system states over which a pattern must hold) that allows a user to generate formal specifications by using direct substitution of propositions into parameters of selected patterns and scopes. Prospec extended SPS to support the definition of patterns and scopes that include the ability to specify parameters with multiple propositions (referred to as composite propositions or CPs), allowing the specification of sequential and concurrent behavior. Prospec generates formal specifications in Future Interval Logic (FIL) using direct substitution of CPs into pattern and scope parameters. While substitution works trivially for FIL, it does not work for Linear Temporal Logic (LTL), a highly expressive language that supports specification of software properties such as safety and liveness. LTL is important because of its use in the model checker Spin, the ACM 2001 system Software Award winning tool, and NuSMV. This paper introduces abstract LTL templates to support automated generation of LTL formulas for complex properties in Prospec. In addition, it presents formal proofs and testing to demonstrate that the templates indeed generate the intended LTL formulas.

► Defined templates for large number of complex LTL specs. The templates are built on the Specification Pattern System.
► Described the approach for using direct substitution of propositions into the templates to arrive at the desired spec.
► Defined new LTL operators to simplify the description of the LTL templates.
► Used first order logic to prove correctness of generated LTL specs against original patterns, scopes, and CP classes.
► Defined a new model checking based testing approach to test the correctness of generated LTL specs.