Specification patterns for finite-state verification

From Wikipedia, the free encyclopedia

This article may need to be wikified to meet Wikipedia's quality standards.
Please help improve this article, especially its introduction, section layout, and relevant internal links. (help)

The introduction to this article provides insufficient context for those unfamiliar with the subject matter.
Please help improve the introduction to meet Wikipedia's layout standards. You can discuss the issue on the talk page.

Contents

[edit] 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.

[edit] Specification Pattern System

The Specification Pattern System discussed in [1] recognizes that 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.

[edit] 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 \Diamond P \to (\lnot P ~\mathcal{U}~ (S \land \lnot P))
Before R \Diamond R \to (\lnot P ~\mathcal{U}~ (S \lor R))
After Q \Box \lnot Q \lor \Diamond(Q \land (\lnot P ~\mathcal{U}~ (S \lor \Box \lnot P)))
Between Q and R \Box ((Q \land \Diamond R) \to (\lnot P ~\mathcal{U}~ (S \lor R)))
After Q until R \Box (Q \to ((\lnot P ~\mathcal{U}~ (S \lor R)) \lor \Box \lnot P))

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.

[edit] 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.


[edit] 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/


[edit] 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.


[edit] See also

[edit] External sources

[1] M. Dwyer, G. Avrunin, J. Corbett, Patterns in Property Specification for Finite-State Verification. In Proceedings of the 21st International Conference on Software Engineering, pages 411-420, May 1999.

[edit] External links

Retrieved from "http://en.wikipedia.org../../../s/p/e/Specification_patterns_for_finite-state_verification.html"