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
Formal Methods Virtual Library
for information about a wide variety of finite-state verification tools.
People involved in the Project
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 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.
- 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.
- 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.
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.
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
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.
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
DOMAIN: feature integration, elevator
illustrates the kind of information recorded (english language description,
pattern, scope, formal spec, developer of the spec, citation, and
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, ...).
- "After every occurrence of X there must be an occurrence of Y."
- "Between a P and a Q there can never be an X."
You can email.
example requirements or citations/references to such requirements to us.
If you have any comments/criticisms/suggestions/... you can
We'd like to hear about your experiences.
So far people have visited.
This work is partially funded by NSF under grants
CCR-9308067, CCR-9407182, CCR-9708184 and
CCR-9703094 and by NASA under award
Last updated Sept 1998.