About Specification Patterns

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.