Specification patterns for finite-state verification
|
|
| Contents |
Motivation for Patterns in Property Specification
The formal verification of the properties of concurrent systems requires expressing the system requirements in the specification language of the verification tool. Linear temporal logic formulas are commonly used to express such properties (see Temporal logic in finite-state verification).
The observation has been made that the LTL formulas required to specify system properties can be difficult to read and understand [1].
The authors of [1] argue that most of the temporal properties of concurrent systems are cases of a small set of general specification patterns. By abstracting the solution to these common specification problems in the form of patterns, it is believed this will increase support for automated verification tools.
Specification Pattern System
The Specification Pattern System discussed in [1] recognizes the certain requirements occur in many systems, and formal specification of these requirements can be abstracted into a pattern. These patterns can be thought of as a high-level toolkit that allows the builders of formal models to quickly find the correct formal expression of the requirement in their particular specification language.
Property Specification Patterns
The authors of [1], in their specification pattern system, define patterns as having the following elements:
- name
- intent of pattern
- mapping to known formalisms
- examples of known uses
- relationship to other patterns
A key section is the mapping to known formalisms. Once a requirement has been recognized as a pattern, the template for the formal expression in a particular specification language can be mechanically produced.
In [1], the Precedence pattern is given as an example. In Precedence, state S must appear before state P. The Precedence pattern includes the following formal expressions in linear temporal logic (LTL):
LTL S precedes P:
| Globally | <math>\Diamond P \to (\lnot P ~\mathcal{U}~ (S \land \lnot P))<math> |
| Before R | <math>\Diamond R \to (\lnot P ~\mathcal{U}~ (S \lor R))<math> |
| After Q | <math>\Box \lnot Q \lor \Diamond(Q \land (\lnot P ~\mathcal{U}~ (S \lor \Box \lnot P)))<math> |
| Between Q and R | <math>\Box ((Q \land \Diamond R) \to (\lnot P ~\mathcal{U}~ (S \lor R)))<math> |
| After Q until R | <math>\Box (Q \to ((\lnot P ~\mathcal{U}~ (S \lor R)) \lor \Box \lnot P))<math> |
The line "Globally" represents the property that the S must precede P within the entire execution of the program. The meaning of the other lines are discussed below (see scope).
In the example given in [1], the formalisms for the Precedence pattern are not restricted to LTL. Formalism of the pattern in computational tree logic (CTL) and regular expressions are also given. (See the Precedence Pattern). As specification languages evolve, the 'library' of known formalisms associated with the pattern will grow.
Pattern Scope
PatternScope.JPG
Pattern Scope
The authors of [1] define scope as "the extent of the program execution over which the pattern must hold."
Scope expresses a pattern's relationship to other states/events within the execution of a program.
For example, between Q and R means a given pattern must occur between two other states.
The notion of scope allows the specification of complex temporal properties to be built from a relatively simple set of patterns.
Pattern Hierarchy
The authors of [1] "..believe the most useful way to organize the patterns is in a hierarchy based on their semantics." The purpose is to help designers of formal models identify the patterns that formally express their requirements.
The hierarchy of patterns is broken up into two main categories: occurrence and order (see diagram from [1] below).
A detailed description of the various patterns can be found in the external link: http://patterns.projects.cis.ksu.edu/
PatternHierarchy.JPG
Pattern Usability
Research in [1] claims that out of 555 property specifications examined, 92% were cases of the patterns identified by the authors. This supports the notion of a system of patterns as a tool for developing property specifications for finite-state verification.
See Also
- Linear temporal logic
- Formal verification
- Finite-state verification
- Model checking
- Concurrent systems
External Sources
[1] M. Dwyer, G. Avruin, J. Corbett, Y. Hu, Patterns in Property Specification for Finite-State Verification. In M. Ardis, editor, Proceedings of the Second Workshop on Formal Methods in Software Practice, pages 7-15, Mar. 1998.