Automated formal specification generation and refinement from requirement documents
AUTOR(ES)
Cabral, Gustavo, Sampaio, Augusto
FONTE
Journal of the Brazilian Computer Society
DATA DE PUBLICAÇÃO
2008-03
RESUMO
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.
Documentos Relacionados
- Formal specification and verification of real-time systems using Graph Grammars
- Especificação formal de organizações de sistemas multiagentes
- PhyloGenie: automated phylome generation and analysis
- Minimal Hyperlinking Hytime Documents: Specification and Browsing of Classic Hypertext Structures
- Automated Encoding of Clinical Documents Based on Natural Language Processing