Formalising Software Requirements using Large Language Models

• URL: http://arxiv.org/abs/2506.10704v1
• Date: Thu, 12 Jun 2025 13:55:01 GMT
• Title: Formalising Software Requirements using Large Language Models
• Authors: Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan,
• Abstract summary: The project addresses the challenges in the traceability and verification of formal specifications.<n>It provides support for the automatic generation of the formal specifications and the traceability of the requirements from the initial software design stage through the systems implementation and verification.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper is a brief introduction to our recently initiated project named VERIFAI: Traceability and verification of natural language requirements. The project addresses the challenges in the traceability and verification of formal specifications through providing support for the automatic generation of the formal specifications and the traceability of the requirements from the initial software design stage through the systems implementation and verification. Approaches explored in this project include Natural Language Processing, use of ontologies to describe the software system domain, reuse of existing software artefacts from similar systems (i.e. through similarity based reuse) and large language models to identify and declare the specifications as well as use of artificial intelligence to guide the process.

Related papers

• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1 aims to investigate automated and semi-automated approaches to bridge this gap.<n>This position paper presents a preliminary synthesis of relevant literature to identify recurring challenges and prospective research directions.
  arXiv  Detail & Related papers  (2025-07-18T19:15:50Z)
• A Short Survey on Formalising Software Requirements using Large Language Models [0.0]
  This paper presents a focused literature survey on the use of large language models (LLM) to assist in writing formal specifications for software.<n>A summary of thirty-five key papers is presented, including examples for specifying programs written in Dafny, C and Java.
  arXiv  Detail & Related papers  (2025-06-13T15:26:58Z)
• Semi-Automated Design of Data-Intensive Architectures [49.1574468325115]
  This paper introduces a development methodology for data-intensive architectures.<n>It guides architects in (i) designing a suitable architecture for their specific application scenario, and (ii) selecting an appropriate set of concrete systems to implement the application.<n>We show that the description languages we adopt can capture the key aspects of data-intensive architectures proposed by researchers and practitioners.
  arXiv  Detail & Related papers  (2025-03-21T16:01:11Z)
• Validation of Rigorous Requirements Specifications and Document Automation with the ITLingo RSL Language [0.0]
  ITLingo initiative has introduced a requirements specification language named RSL to enhance the rigor and consistency of technical documentation. This paper reviews existing research and tools in the fields of requirements validation and document automation. We propose to extend RSL with validation of specifications based on customized checks, and on linguistic rules dynamically defined in the RSL itself.
  arXiv  Detail & Related papers  (2023-12-17T21:39:26Z)
• Language Models as a Service: Overview of a New Paradigm and its Challenges [47.75762014254756]
  Some of the most powerful language models currently are proprietary systems, accessible only via (typically restrictive) web or programming. This paper has two goals: on the one hand, we delineate how the aforementioned challenges act as impediments to the accessibility, replicability, reliability, and trustworthiness of LM interfaces. On the other hand, it serves as a comprehensive resource for existing knowledge on current, major LM, offering a synthesized overview of the licences and capabilities their interfaces offer.
  arXiv  Detail & Related papers  (2023-09-28T16:29:52Z)
• Natural Language Processing for Requirements Formalization: How to Derive New Approaches? [0.32885740436059047]
  We present and discuss principal ideas and state-of-the-art methodologies from the field of NLP. We discuss two different approaches in detail and highlight the iterative development of rule sets. The presented methods are demonstrated on two industrial use cases from the automotive and railway domains.
  arXiv  Detail & Related papers  (2023-09-23T05:45:19Z)
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models [3.1143846686797314]
  We present nl2spec, a framework for applying Large Language Models (LLMs) derive formal specifications from unstructured natural language. We introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization.
  arXiv  Detail & Related papers  (2023-03-08T20:08:53Z)
• Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
  This article examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use. It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools.
  arXiv  Detail & Related papers  (2023-01-05T18:18:46Z)
• Technical Report on Neural Language Models and Few-Shot Learning for Systematic Requirements Processing in MDSE [1.6286277560322266]
  This paper is based on the analysis of an open-source set of automotive requirements. We derive domain-specific language constructs helping us to avoid ambiguities in requirements and increase the level of formality.
  arXiv  Detail & Related papers  (2022-11-16T18:06:25Z)
• Natural Language Processing for Systems Engineering: Automatic Generation of Systems Modelling Language Diagrams [0.10312968200748115]
  An approach is proposed to assist systems engineers in the automatic generation of systems diagrams from unstructured natural language text. The intention is to provide the users with a more standardised, comprehensive and automated starting point onto which subsequently refine and adapt the diagrams according to their needs.
  arXiv  Detail & Related papers  (2022-08-09T19:20:33Z)
• Using Document Similarity Methods to create Parallel Datasets for Code Translation [60.36392618065203]
  Translating source code from one programming language to another is a critical, time-consuming task. We propose to use document similarity methods to create noisy parallel datasets of code. We show that these models perform comparably to models trained on ground truth for reasonable levels of noise.
  arXiv  Detail & Related papers  (2021-10-11T17:07:58Z)
• Exploring Software Naturalness through Neural Language Models [56.1315223210742]
  The Software Naturalness hypothesis argues that programming languages can be understood through the same techniques used in natural language processing. We explore this hypothesis through the use of a pre-trained transformer-based language model to perform code analysis tasks.
  arXiv  Detail & Related papers  (2020-06-22T21:56:14Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.