Working Document -- Formalising Software Requirements with Large Language Models

TL;DR

This working document reviews 94 papers on formalising software requirements using large language models, covering traceability, formal methods, and theoretical frameworks, aiming to advance understanding and tools in software requirements engineering.

Contribution

It provides a comprehensive survey and analysis of recent research on formalising software requirements with large language models, integrating theories and tools for improved requirement traceability and formal verification.

Findings

Reviewed 94 papers on formalising requirements

Discussed integration of formal methods and LLMs

Highlighted gaps and future research directions

Abstract

This draft is a working document, having a summary of nighty-four (94) papers with additional sections on Traceability of Software Requirements (Section 4), Formal Methods and Its Tools (Section 5), Unifying Theories of Programming (UTP) and Theory of Institutions (Section 6). Please refer to abstract of [7,8]. Key difference of this draft from our recently anticipated ones with similar titles, i.e. AACS 2025 [7] and SAIV 2025 [8] is: [7] is a two page submission to ADAPT Annual Conference, Ireland. Submitted on 18th of March, 2025, it went through the light-weight blind review and accepted for poster presentation. Conference was held on 15th of May, 2025; [8] is a nine page paper with additional nine pages of references and summary tables, submitted to Symposium on AI Verification (SAIV 2025) on 24th of April, 2025. It went through rigorous review process. The uploaded version on arXiv.org [8] is the improved one of the submission, after addressing the specific suggestions to improve the paper.