Verication of Automatically Generated Pattern-Based LTL Specications

The use of property classications and patterns, i.e., high-level abstractions that describe common behavior, have been shown to assist practitioners in generating for-mal specications that can be used in formal verication techniques. The Specication Pattern System (SPS) pro-vides descriptions of a collection of patterns. The extent of program execution over which a pattern must hold is de-scribed by the notion of scope. SPS provides a manual tech-nique for obtaining formal specications from a pattern and a scope. The Property Specication Tool (Prospec) extends SPS by introducing Composite Propositions (CPs), a clas-sication for dening sequential and concurrent behavior to represent pattern and scope parameters, and provides a tool to support users