PROPEL: An approach supporting user guidance in developing precise and understandable property specifications

Property specifications are often used in requirements engineering to concisely describe a single aspect of system behavior. Although each property has a narrow focus, it can still be difficult to specify a property correctly. There are often subtle, but important, details in desired system behavior that can easily be overlooked, and there is little guidance available for how to avoid such mistakes. In addition to capturing these details correctly, property specifications should be (a) precise enough to support automated analyses that can be used to check that actual system behavior is consistent with the specifications, and (b) understandable enough to be readily comprehended by all system developers. Property specifications can be written in a mathematical formalism, which provides precision, but such formalisms are often difficult to understand. Thus, in practice, property specifications tend to be written in natural language. Property specifications written with such informality are often ambiguous, however, and usually cannot be used in many types of automated analyses.^ To address these challenges, our approach supports elicitation and specification of properties by providing templates that build on commonly-occurring property patterns. These templates offer guidance by explicitly indicating the variations that must be considered, thereby ensuring that important subtle details are not overlooked. To support the use of this approach, we developed PROPEL, for PROPerty ELucidator. PROPEL provides three alternative views that users can work with to specify properties: graphical finite-state automata, which offer precision; disciplined natural language, which offers understandability; and question trees, which offer guidance for selecting a template. ^ To evaluate this approach, we used PROPEL to specify properties in five case studies in the medical domain. The case studies showed that our approach was effective at specifying the vast majority of the properties we encountered. We also undertook a small empirical study that showed that the disciplined natural language view of the properties was usually understood. These results indicate that our approach to property elicitation and specification is a promising one.