Proceedings Template - WORD

1
P
ROPEL
: An Approach Supporting Property Elucidation

Rachel L. Smith, George S. Avrunin, Lori A. Clarke, and Leon J. Osterweil
Department of Computer Science
University of Massachusetts
Amherst, Massachusetts 01003
(413) 545-2013
{rasmith, avrunin, clarke, ljo}@cs.umass.edu


ABSTRACT

Property specifications concisely describe what a software system
is supposed to do. It is surprisingly difficult to write these
properties correctly. There are rigorous mathematical formalisms
for representing properties, but these are often difficult to use. No
matter what notation is used, however, there are often subtle, but
important, details that need to be considered. P
ROPEL
aims to
make the job of writing and understanding properties easier by
providing templates that explicitly capture these details as options
for commonly-occurring property patterns. These templates are
represented using both "disciplined" natural language and finite-
state automata, allowing the specifier to easily move between
these two representations.
1. INTRODUCTION
Finite-state verification approaches, such as model checking,
determine if the behavior of a hardware or software system is
consistent with a specified property. Instead of specifying the full
behavior of the system, each property may focus on one particular
aspect of system behavior. These properties may be written in a
number of different specification formalisms, such as temporal
logics, graphical finite-state machines, or regular expression
notations, depending on the finite-state verification system that is
being employed. Although there are sometimes theoretical
differences in the expressive power of these languages, these
differences are rarely encountered in practice. A serious problem
that is frequently encountered in practice, however, is expressing
the intended behavior of the system correctly. Even though
properties usually focus on some restricted aspect of a system's
behavior, it is still surprisingly difficult to capture this behavior
precisely. These properties are often "almost" correct, but fail to
capture some important, and sometimes subtle, aspects of the
system's intended behavior. Often these aspects are not revealed
until testing or verification. Thus, analysts frequently spend a
considerable amount of time trying to verify a property, only to
later determine that the property has been specified incorrectly.
Software developers tend to avoid the more mathematical
property specification formalisms and instead write requirements
and design specification documents in natural language, perhaps
sprinkled with some tabular or graphical notations. Although
these documents seem to be more accessible to practitioners, they
are usually very verbose and contain impreciseand sometimes
ambiguous and inconsistentdescriptions of the system. Thus,
they are of limited value when doing rigorous analysis of the
system.
What is needed is a property specification approach that is not
only accessible to developers, but is also mathematically precise,
so that it can be used as the basis for verification and other types
of analysis. Recent work on property patterns [8-10] recognized
that the properties used in formal verification often map onto one
of several basic property patterns. These patterns can be
instantiated with specific events or states and then mapped to
several different formalisms. When we tried to employ these
property patterns to represent some actual natural language
requirements, however, we found that they were not adequate.
They failed to represent some of the subtle differences in
interpretation that we encountered.
In the work presented here, we build upon the property patterns in
several important ways. First, we extend the patterns so that they
are represented by pattern templates. Thus, instead of just
parameterizing the pattern in terms of the events or states, we
extend the patterns with alternative options that are explicitly
shown to the specifier. Choosing among these options should help
the specifier consider the relevant alternatives and subtleties
associated with the intended behavior. Second, we represent these
pattern templates using two different notations: an extended
finite-state automaton (FSA) representation and a disciplined
natural language (DNL) representation. Both of these
representations have some advantages. The DNL representation
provides a short list of alternative phrases that highlight the
options, as well as synonyms for each option to support
customization. This representation should appeal to those
specifiers who prefer a natural language description. The extended
FSA representation provides a graphical view that can be used to
derive an instantiation of a specific FSA representation. It too
helps the specifier see the options that need to be considered.
Third, the instantiated FSA representation is mathematically well-
defined and thus can be used as the basis for verification, as well
as for testing the acceptance of event sequences, validating the
consistency of a set of property automata, or other types of
analysis. Finally, we believe that providing specifiers with the
ability to view both representations simultaneously and select the
available options from either representation will help them to
elucidate the desired property. We are currently developing a



2
system, called P
ROPEL
, for "PROPerty ELucidation," that provides
support for specifying properties based on the property pattern
templates, using these two complementary representations.
This paper describes property pattern templates and the P
ROPEL

system. The next section of the paper reviews property patterns
and explains the concerns that motivated the extension to the
templates. Section 3 describes the property pattern templates in
both the FSA and the DNL representations and presents a detailed
example for one of the patterns, using both forms. Section 4
details an example of the specification process using P
ROPEL
.
Section 5 addresses how we can incorporate scopes into the
property pattern template representations. Section 6 discusses
related work and Section 7 concludes with a discussion of
limitations and future directions.

2. The Property Patterns
Dwyer, Avrunin, and Corbett [8-10] developed a system of
property patterns to assist users of finite-state verification tools,
such as SPIN [18], SMV [21], INCA [4], and FLAVERS [11].
They argued that the difficulty of writing correct properties in the
various input formalisms used by such tools was a substantial
obstacle to the adoption of finite-state verification technology,
and they proposed the pattern system as a way to capture the
experience of expert specifiers and to enable the transfer of that
experience to other practitioners.
Although the input formalisms of the various finite-state
verification tools, such as the temporal logics LTL and CTL [3]
are very expressive, Dwyer et al. observed that nearly all the
properties found in the finite-state verification literature could be
classified into a small number of basic types, and suggested that a
collection of patterns, which they described as "high-level,
formalism-independent, specification abstractions," could assist
finite-state verification practitioners in formulating most of the
properties they wanted to check.
Each of the patterns describes an intent (the structure of the
specified behavior), a scope (the extent of program execution over
which the pattern must hold), mappings into the input formalisms
for some finite-state verification tools, examples of known uses,
and relationships to other patterns. For instance, the intent of the
Response pattern is a cause-and-effect relationship between a pair
of events or states, in which the occurrence of the "cause" or
"action" leads to an occurrence of the "effect" or "response."
Dwyer et al. identified five scopes, or segments of program
execution, in which the specifier might want to insist that the
specified intent holds. For instance, a particular Response relation
might be intended to hold only while the system is executing in a
certain mode, while instances of the action might require an
entirely different response in other modes. Th