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.

• Publication year

  2008

• Venue

  Journal of the Brazilian Computer Society

• Publication date

  2008-03-01

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1007/BF03192554
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Failures-divergence Refinement Fdr2 User Manual

  2012influential reference
• The unified modeling language reference manual

  2010influential reference
• NLForSpec: Translating Natural Language Descriptions into Formal Test Case Specifications

  2007influential reference
• Formal Specification Generation from Requirement Documents

  2006cited by this paper
• Automatic Translation from Circus to Java

  2006cited by this paper
• How UML is used

  2006cited by this paper
• Viewing CSP Specifications with UML-RT Diagrams

  2006influential reference
• Reasoning about inconsistencies in natural language requirements

  2005cited by this paper
• Towards Formal Specification and Generation of Autonomic Policies

  2005cited by this paper
• Model-Based Testing in Practice

  2005cited by this paper
• A strategy for the formal composition of frameworks

  2005cited by this paper
• Specification-driven automated testing of GUI-based Java programs

  2004cited by this paper
• DERIVING BEHAVIOR SPECIFICATIONS FROM TEXTUAL USE CASES

  2004cited by this paper
• Tutorial: an overview of UML 2.0

  2004cited by this paper
• Office 2003 XML - integrating office with the rest of the world

  2004cited by this paper
• Inside Microsoft Visual Studio .Net

  2003cited by this paper
• ECOLE: a look-ahead editor of controlled language

  2003influential reference
• Message Sequence Charts

  2003cited by this paper
• Tutorial: an overview of UML 2

  2003influential reference
• MDA explained - the Model Driven Architecture: practice and promise

  2003cited by this paper
• Cost Effective Uses of Formal Methods in Verification and Validation

  2002cited by this paper
• Cost Effective Use of Formal Methods in Verification and Validation

  2002cited by this paper
• CSP Networking for Java (JCSP.net)

  2002cited by this paper
• Automated conversion from requirements documentation to an object-oriented formal specification language

  2002cited by this paper
• Process Oriented Design for Java: Concurrency for All

  2002cited by this paper
• Writing effective use cases

  2001cited by this paper
• Animating CSPm using Action Semantics

  2001cited by this paper
• Writing Effective Use Cases

  2000cited by this paper
• A Method for Requirements Elicitation and Formal Specification

  1999cited by this paper
• A Systematic and Traceable Progression from Scenario Models to Communicating Hierarchical State Machines

  1999cited by this paper
• Controlled natural language can replace first-order logic

  1999cited by this paper
• Model Checking of Message Sequence Charts

  1999cited by this paper
• Formal verification with natural language specifications: guidelines, experiments and lessons so far

  1999cited by this paper
• Guiding the Construction of Textual Use Case Specifications

  1998cited by this paper
• Attempto Controlled English - Not Just Another Logic Specification Language

  1998cited by this paper
• Use Case Maps as Architectural Entities for Complex Systems

  1998cited by this paper
• The Theory and Practice of Concurrency

  1997cited by this paper
• Java Language Reference

  1997cited by this paper
• Modelling and verifying key-exchange protocols using CSP and FDR

  1995cited by this paper
• Specifying Logic Programs in Controlled Natural Language

  1995cited by this paper
• FRAME SEMANTICS AND THE NATURE OF LANGUAGE *

  1976cited by this paper

• The MERLIN Method to Create Modeling Assistants for Model-Driven Development Tools

  2022influential citation
• A framework for automatic development of embedded system

  2017cites this paper
• Model-based documentation

  2017cites this paper
• Melhoria de Documentos de Requisitos: um Mapeamento Sistemático da Literatura

  2016cites this paper
• Formal analysis of confidentiality conditions related to data leakage

  2016cites this paper
• Computer-Aided Formalization of Requirements Based on Patterns

  2014cites this paper
• Generating Logical Specifications from Requirements Models for Deduction-based Formal Verification

  2014cites this paper
• Pengembangan Tools pada Fase Requirement Engineering dengan Metode LWBA

  2014cites this paper
• A Strategy to Formalize Specification and Its Application to an Advanced Railway System

  2014cites this paper
• Guided Requirements Clarification for Automatic Formalization

  2013cites this paper
• Deduction-Based Formal Verification of Requirements Models with Automatic Generation of Logical Specifications

  2012cites this paper
• Proposal to Improve the Requirements Process through Formal Verification using Deductive Approach

  2012cites this paper
• Towards Refinement Strategy Planning for Event-B

  2012cites this paper