The automata and temporal-logic formalisms that are commonly used to describe state and event sequencing properties of concurrent systems can be subtle and difficult to use correctly. Even people with significant experience with temporal logics find it difficult to specify common software requirements in their formalism of choice. Consequently it is a significant challenge to make these formalisms amenable to effective use by practicing software developers.
To address this issue, in previous work [3] we identified a small number of commonly occurring classes of temporal requirements, e.g., invariance, response, and precedence properties. We refer to these classes as specification patterns; there are five basic patterns:
In developing this system of patterns we found that it was useful to distinguish the required pattern of states/events from the region of system execution in which this pattern was required. Pattern scopes define variations of the basic patterns in which checking of the pattern is disabled during specified regions of execution. There are five basic scopes; a pattern can hold
In subsequent work [7], we validated that these specification patterns were representative of a large majority of the temporal requirements that researchers and users of finite-state verification tools had written. We studied over 600 property specifications and found that over 94% were instances of the patterns; interestingly over 70% of the properties were either universal or response properties.
We believe that there are several advantages to a pattern based approach. It can shorten the learning curve by presenting a smaller collection of concepts to specification writers. These patterns are expressible in nearly all of the commonly used specification languages for existing finite-state verification tools, thus, patterns provide some degree of tool independence. Finally, techniques for optimizing the construction of finite-state models can exploit information about the structure of the patterns.
BSL builds off of this work by providing a structured-English language front-end for the patterns which is illustrated in the fourth and fifth rule sets of Figure 19. Common synonyms are supported. For example, invariance and universal patterns and leads to can be used to express the FullToNonFull property from Figure 15 as
FullToNonFull: forall[b:BoundedBuffer].
{Full(b)} leads to {!Full(b)} globally
These pattern specifications are then translated into the specification formalism for the chosen checker. For example, if using Spin the leads to part of this property would be translated to the following LTL
[]( {Full(b)} -> <> {!Full(b)} )
Figure 19: BSL Pattern and Quantifier Syntax
Bandera supports user defined extension of BSL patterns. Users can define their own patterns and mappings to low-level specification formalisms. In this way, an expert specifier can customize a collection of patterns for the use of the developers on a project.