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.
The following example specification description illustrates the kind of information recorded (English language description, pattern, scope, formal spec, developer of the spec, citation, and problem domain).
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
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:
If possible, we would like to collect additional temporal specifications as both natural language descriptions of the requirements as well as expressions of requirements in a formal specification language (e.g., LTL, CTL, regular expressions, ...).