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.
Main Authors: | , |
---|---|
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!
|