A Specification Pattern System

A Specification Pattern System


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 already support mappings to a number of formalisms that have tool support for automated analysis.

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. In fact this has already happened a few times.

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.

See the Formal Methods Virtual Library for information about a wide variety of finite-state verification tools.


People involved in the Project


Papers

This paper gives an introduction to the patterns system. This paper gives a brief overview of our updated pattern system, describes our survey of property specifications, and presents the results of the survey (extracted from the raw data that is linked below).

The Patterns

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


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. We only supplying the mappings on these formalism-specific 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 resources that provide (at least) anecdotal evidence of the utility of the patterns and examples of how they can be applied.

Some papers reporting on applications of FSV that use patterns.


Survey of Property Specifications

As part of the property specification patterns project we have conducted a survey of how people are using specification formalisms supported by FSV tools. The goal is to evaluate the utility of the patterns. We solicited contribution, in the Spring of 1998, of examples of requirements that might be verified with existing finite-state verification tools (e.g., SPIN, SMV, CWB-NC, INCA, FLAVERS, ...). We received a number of responses and have surveyed the literature to collect a number of specifications.

A paper describing the survey and the interpretation of its results is provided above. Descriptions of each of the collected specifications are given in this directory.

This example specification description:

REQUIREMENT: Pressing a landing button guarantees that the lift will arrive
             at that landing with its doors open.
PATTERN: Response
SCOPE: Global
LTL: AG(landingButi.pressed -> AF(lift.floor=i & lift.door=open))
NOTES: This is an examplar for a class of specs for each floor i
SOURCE: M. Ryan
CITE: \cite{ryan:97}
DOMAIN: feature integration, elevator
illustrates the kind of information recorded (english language description, pattern, scope, formal spec, developer of the spec, citation, and problem domain).

We are continuing to collect this survey data and will periodically update this part of the web-site. If you'd like to make a contribution we'd be happy to accept your requirements. The kind of requirements we are interested in typically restrict the occurrence/order of states/events in the finite-state model of the system. Examples include:

We are interested in both natural language descriptions of the requirements as well as expressions of requirements in a formal specification language (e.g., LTL, CTL, regular expressions, ...).

You can email. example requirements or citations/references to such requirements to us.


Feedback

If you have any comments/criticisms/suggestions/... you can email us. 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, CCR-9708184 and CCR-9708184, CCR-9703094 and by NASA under award NAG-2-1209.
Last updated Sept 1998.