Temporal 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.
Documentation
About
This site was hosted at Kansas State University for many years.
Extensions
The original pattern system, which is described on these pages, has been built on by a number of others to target specific problem domains and to incorporate additional expressive power.