Formal Specification Generation from Requirement Documents

Automatic generation of formal specifications from requirement reduces cost and complexity of formal models creation. Thus, the generated formal model brings the possibility to carry out system property verification. This paper proposes a Controlled Natural Language (CNL, a subset of English), use case specification templates, and a strategy and tool support to generate process algebraic formal models (in CSP notation) from use cases specified using the templates and CNL. We define templates that represent ent at different levels of abstraction. Moreover, a refinement notion is defined based on events between abstract and concrete models.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Gustavo Cabral, Augusto Sampaio
• Keywords: Controlled Natural Language, ENTCS 2008, Formal Models, Generated Formal Model