Automated formal specification generation and refinement from requirement documents

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.

Saved in:
Bibliographic Details
Main Authors: Cabral,Gustavo, Sampaio,Augusto
Format: Digital revista
Language:English
Published: Sociedade Brasileira de Computação 2008
Online Access:http://old.scielo.br/scielo.php?script=sci_arttext&pid=S0104-65002008000100008
Tags: Add Tag
No Tags, Be the first to tag this record!