From Natural Language Requirements to Rigorous Property Specifications

Abstract − Property specifications concisely describe selected aspects of what a software system is supposed to do. It is surprisingly difficult to write these properties correctly. Although there are rigorous mathematical formalisms for representing properties, 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. The PROPEL tool 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 “disciplined ” natural language, decision trees, and finite-state automata, allowing the developer to easily move between these representations. I