Facilitating the construction of specification pattern-based properties

Formal specification languages are often perceived as difficult to use by practitioners, and are therefore rarely-used in industrial software development practices. Numerous researchers have developed specification pattern systems to facilitate the construction of formal specifications of system properties. Feedback indicates that these patterns are considered helpful, but many practitioners prefer capturing properties using informal notations, such as natural language, instead of formal specification languages. This paper describes a project that addresses this technology gap. First, we introduce a stepwise process for deriving and instantiating system properties in terms of their natural language representations. The key components of this process are structured natural language grammars and specification pattern systems. Second, we describe SPIDER, a prototype implementation of a tool suite supporting this specification process. We illustrate the use of our approach with a description of a stepwise construction process of property specifications of a real-world automotive embedded system using Spider.