A Specification Pattern System

These pages are under construction. They could undergo drastic changes in terms of organization and content in the next few months. Eventually we hope the structure will become fixed, but that additional useful material will continue to be added.

This page is the home of an online repository for information about property specification for finite-state verification. The intent of this repository is to collect patterns that occur commonly in the specification of concurrent and reactive systems. Most specification formalisms in this domain are a bit tricky to use. To make them easier to use our patterns come with descriptions that illustrate how to map well-understood, but imprecise, conceptions of system behavior into precise statements in common formal specification languages. We're currently planning on mappings to a number of formalisms that have tool support for automated analysis (see the list below for our current plans).

This isn't a static repository. We imagine that additional formalisms may be supported, the set of patterns will be extended, and different organizations of the patterns will be produced catering to different users.

Hopefully lots of people will contribute to and use the information on these pages.

We've collected and answered some frequently asked questions about the specification pattern system. If you have additional questions/comments please send them along to us.

People involved in the Project

Papers

Property Specification Patterns for Finite-state Verification, Matthew B. Dwyer, George S. Avrunin and James C. Corbett in the 2nd Workshop on Formal Methods in Software Practice, March, 1998. An abstract of this paper is also available.

The Patterns

The information in the patterns can be presented in a variety of ways. Our first organization, illustrated below, is based on classifying the patterns in terms of the kinds of system behaviors they describe.

Occurrence Patterns talk about the occurrence of a given event/state during system execution.
Order Patterns talk about relative order in which multiple events/states occur during system execution.
Chain Patterns talk about building more complex behavior descriptions out of order and occurrence patterns.
While not themselves patterns, Pattern Notes discuss common ways to vary the existing patterns to suite your needs.

An alternative organization for this information is to group pattern to formalism mappings by specification formalism. The supported formalisms are listed below. Clicking on the formalism will bring you to pages with mappings for each property pattern in that formalisms. Right now we're only supplying the mappings on those pages and you are refered to the complete patterns for information about relationships and example uses.

Pattern Usage

We are making use of the patterns in our applied FSV research. We'll be linking a variety of different specification case studies that have been developed. These serve as both anecdotal evidence of the utility of the patterns and examples of how they can be applied.

LTL specifications for a generic concurrent software component

Feedback

If you use these patterns in some significant way drop us some email. We'd like to hear about your experiences.

So far people have visited.

Thanks

This work is partially funded by NSF under grants CCR-9308067, CCR-9407182, and CCR-9703094.

Last updated Feb 1998.