Property Patterns: One important obstacle to using temporal logic is the difficulty of expressing complex properties correctly. Dwyer and his colleagues have proposed a pattern-based approach to the presentation, codification, and reuse of property specifications for finite-state verification (Dwyer, Avrunin, and Corbett 1998; Dwyer, Avrunin, and Corbett 1999) and (Spec Patterns website).
The patterns enable non-experts to read and write formal specifications for realistic systems (including reactive systems) and facilitate easy conversion of specifications between different formalisms.
The system allows patterns like “P is absent between Q and S” or “S precedes P between Q and R” to be easily expressed in and translated between Linear Temporal Logic (LTL) (Manna and Pnueli 1990), Computation Tree Logic (CTL) (Clarke et al. 1986), Quantified Regular Expressions (QRE) (Olender and Osterweil 1990), and other state-based and event-based formalisms. (Dwyer, Avrunin, and Corbett 1999) also performed a large-scale study in which specifications containing over 500 temporal properties were collected and analyzed. They noticed that over 90% of these could be classified under one of the proposed patterns.