Attempto - From Specifications in Controlled Natural Language towards Executable Specifications

TL;DR

This paper introduces Attempto, a system that transforms specifications written in controlled natural language ACE into formal logic and executable code, bridging informal requirements and formal specifications for verification and simulation.

Contribution

It presents a novel approach using controlled natural language to create formal, executable specifications that are both human-readable and machine-processable.

Findings

ACE specifications can be accurately translated into logic and Prolog

The system enables verification, simulation, and validation of specifications

Controlled natural language improves accessibility of formal methods

Abstract

Deriving formal specifications from informal requirements is difficult since one has to take into account the disparate conceptual worlds of the application domain and of software development. To bridge the conceptual gap we propose controlled natural language as a textual view on formal specifications in logic. The specification language Attempto Controlled English (ACE) is a subset of natural language that can be accurately and efficiently processed by a computer, but is expressive enough to allow natural usage. The Attempto system translates specifications in ACE into discourse representation structures and into Prolog. The resulting knowledge base can be queried in ACE for verification, and it can be executed for simulation, prototyping and validation of the specification.