Formalising Software Requirements using Large Language Models

TL;DR

This paper introduces the VERIFAI project, which leverages large language models and AI techniques to improve the traceability and verification of natural language software requirements by automating formal specification generation.

Contribution

It presents a novel approach combining NLP, ontologies, reuse of artifacts, and AI-guided processes to enhance software requirements formalization and traceability.

Findings

Initial exploration of LLMs for formal requirement specification

Use of ontologies to improve domain modeling

AI-guided verification process development

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.