TITLE: Property Specification Patterns for Finite-state Verification

AUTHOR: Matthew B. Dwyer, George S. Avrunin, and James C. Corbett

AFFILIATION: Department of Computing and Info. Sciences 
             Kansas State University

             Department of Mathematics and Statistics
             University of Massachusetts

             Department of Information and Computer Science 
             University of Hawaii

KEYWORDS:
  Temporal Logic Specifications, Quantified Regular Expressions, 
  Automated Verification, Model Checking, Patterns

ABSTRACT:
  Finite-state verification (e.g., model checking) provides a powerful
  means to detect errors that are often subtle and difficult to
  reproduce.  Nevertheless, the transition of this technology from
  research to practice has been slow.  While there are a number of
  potential causes for reluctance in adopting such formal methods in
  practice, we believe that a primary cause rests with the fact that
  practitioners are unfamiliar with specification processes,
  notations, and strategies.  Recent years have seen growing success
  in leveraging experience with field-tested design and coding patterns.  
  We propose a pattern-based approach to the presentation, codification 
  and reuse of property specifications for finite-state verification.