Towards Development of Complete and Conflict-Free Requirements

Writing requirements is no easy task. Common problems include ambiguity in statements, specifications at the wrong level of abstraction, statements with inconsistent references to types, conflicting requirements, and incomplete requirements. These pitfalls lead to errors being introduced early in the design process. The longer the gap between error introduction and error discovery, the higher the cost associated with the error. To address the growing cost of system development, we introduce a tool called ASSERT (TM) (Analysis of Semantic Specifications and Efficient generation of Requirements-based Tests) for capturing requirements, backed by a formal requirements analysis engine. ASSERT (TM) also automatically generates a complete set of requirements-based test cases. Capturing requirements in an unambiguous way and then formally analyzing them with an automated theorem prover eliminates errors as soon as requirements are written. It also addresses the historical problem that analysis engines are hard to use for someone without formal methods expertise and analysis results are often difficult for the end-user to understand and make actionable. ASSERT (TM)'s major contribution is to bring powerful requirements capture and analysis capability to the domain of the end-user. We provide explainable and automated formal analysis, something we found important for a tool's adoptability in industry.