Using Patterns and Composite Propositions to Automate the Generation of Complex LTL

Property classifications and patterns, i.e., high-level abstractions that describe common behavior, have been used to assist practitioners in specifying properties. The Specification Pattern System (SPS) provides descriptions of a collection of patterns. Each pattern is associated with a scope that defines the extent of program execution over which a property pattern is considered. Based on a selected pattern, SPS provides a specification for each type of scope in multiple formal languages including Linear Temporal Logic (LTL). The (Prospec) tool extends SPS by introducing the notion of Composite Propositions (CP), which are classifications for defining sequential and concurrent behavior to represent pattern and scope parameters. In this work, we provide formal definitions of patterns and scopes when defined using CP classes. In addition, we provide general (abstract) LTL formulas that can be used to generate LTL specifications for all combinations of pattern, scope, and CP classes