Getting the Details Right

Requirement engineering usually involves repeated refinements of the requirements specifications, starting with high-level systems goals and constraints, to more precise and measurable specifications of intended behavior, to detailed, focused statements that provide the basis for formal reasoning. We refer to these more detailed, mathematically rigorous specifications as

property specifications

. Although care must be taken when defining requirements at all these levels of abstraction, it is particularly difficult to accurately capture all the subtle details associated with property specifications. To help understand these decisions, the PROPEL (

PROP

erty

EL

icitation) system [1, 2] provides templates for commonly occurring property patterns [3] in which the options that need to be considered for each pattern are explicitly represented. PROPEL currently provides three views of each template and its associated options: natural language phrases to be selected, a set of hierarchical questions to be answered, or a finite-state automaton with optional labels, transitions, and accepting states to be selected. After all the options have been selected for a template, the finite-state automaton view provides a mathematically precise property specification.