Automated verification of software systems is an important area of current research in both academia and industry. Such methods have the potential to considerably reduce the cost of verification. Such techniques, however, depend on having a formal representation of the system specification, which can be used as a “golden model” or “oracle” from which tests can be generated. Given such a formal representation, a plethora of methods and techniques developed over the last few decades provide a high degree of automation in the verification process. However, formal specifications of systems are the exception rather than the rule in current engineering practice. This limits the applicability of the vast amount of research in formal methods for verification of real-life systems.

This paper addresses this particular gap of constructing a formal representation from an informal specification. The paper limits the scope of the problem to specifications of reactive systems; this is an important class of systems for which the benefits of automated and formal verification has been demonstrated in practice. They also take advantage of the formal nature of specification documents. Such documents use particular idioms and phrases to reduce the contextual ambiguity inherent in natural language sentences to propose a controlled natural language grammar that can be used for specification documents.

The process of constructing a formal model involves first using case grammar theory to parse a sentence into its components (agents, conditions, values, and so on). Each sentence is parsed into a requirement frame. The authors then outline algorithms to translate them into the formalism of a dataflow reactive system (DFRS), which is expressive enough to describe state transitions and delays. Two variants of the DFRS formalism are discussed: a symbolic variant, which is useful as a target of parsing natural language specifications, and an explicit variant, which is more suitable for analysis using algorithms.