Patterns - lgwagner/SpeAR GitHub Wiki
The SpeAR specification language provides capabilities to specify temporal relations among variables in a specification. Some temporal relationships, however, cannot be captured in the SpeAR specification language. Fortunately, SpeAR has the ability to define patterns that can encapsulate more sophisticated temporal operations. This allows the SpeAR specification language to remain simple and easy to read, while still allowing users the powerful expressive capabilities possible in the formal language backing SpeAR, called Lustre.
The notion of formalized Specification Patterns was first introduced by Dwyer, Avrunin, and Corbett in 1998. Early versions of SpeAR focused on supporting a specific subset of specification patterns identified in this work. However, the authors found the patterns to be somewhat limiting; often times one wanted to say something very similar to an existing pattern with minor changes to the initial conditions, or transition behaviors, and the tool was too rigid to allow such changes. The current version of SpeAR resolves that issue by supporting arbitrary patterns. Further, all of the original patterns supported in early versions of SpeAR can be imported as a library, which is available from the Pattern Observers GitHub repository.
In SpeAR 2.0, a pattern is helpful for defining the specifics of how data is manipulated by the element being described. For example, one might want to use a pattern to show that some event A always precedes some other event B. A pattern that implements that ordering is shown in the Examples section. Syntactically, patterns are very similar to nodes in the Lustre language. Each node accepts some inputs and produces some outputs. Further, a node may have local variables that are used in computation. Finally, nodes may contain properties that the user can use to verify the node is constructed correctly.
SpeAR patterns may contain properties that can be used to validate that the pattern behavior is correct. This is done by adding a variable to the pattern of type boolean, assigning it to the expression that one wishes to hold true, and using the --%PROPERTY <name></name> directive to tell SpeAR to verify it. Properties are proven or invalidated by model checking analysis.
Shown are several examples of patterns that might be useful in a specification.
This example shows a pattern that returns true if the input values for a and b only occur in such an order that every occurrence of b is preceded by an occurrence of b (or they happen simultaneously).
This example shows a pattern that counts how many times a boolean input in has been true since the beginning of execution.
This example shows a modification to the previous example that counts how many steps a boolean input in has been consecutively true. If it becomes false, the count is reset to 0.
