The Propel approach aims to make the job of writing and understanding property specifications easier. Property specifications concisely describe important aspects of what a system is supposed to do. Property specifications must be (a) precise enough to support automated analyses (e.g. software verification) that can be used to check that the behavior of a system is consistent with a specified safety-critical property, and (b) accessible enough to allow them to be readily understood by system designers and clients. Mathematical formalisms (e.g. temporal logics), which offer precision, are often difficult to use, and in practice, system designers tend to instead write properties in a natural language (e.g. English). While natural language may offer accessibility, properties written in it are often ambiguous. No matter what notation is used, however, there are often subtle, but important, property details that need to be considered.
In this talk, I will show how the Propel approach can address these issues. Propel provides templates that offer user guidance by explicitly capturing those details as options for commonly-occurring property patterns. Propel provides three alternative representations of these templates: graphical finite-state automata, which offer precision; "disciplined" English sentences, which offer accessibility; and an interactive question tree format, which offers accessibility and additional user guidance.
This talk will be based on joint work with George S. Avrunin and Lori A. Clarke.