Automated formal specification generation and refinement from requirement documents

Abstract

The automatic generation of formal specifications from requirements suppresses the complexity of formal models manual creation and reveals the immediate benefits of its usage, such as the possibility to carry out refinements, and property verification, which contributes to project cost reduction and quality improvement. This paper proposes a Controlled Natural Language (CNL), a subset of English, used to write use case specifications according to a template. From these use cases a complete strategy and tools enable the generation of process algebraic formal models in the CSP notation. We define templates that represent requirements at different levels of abstraction, capturing different views of the system behavior. Moreover, a refinement notion is defined to connect the generated CSP models through an event mapping relation between abstract and concrete models. This notion is further applied to detail use case specifications and to automate its execution.