RE-oriented Model Development with LLM Support and Deduction-based Verification

TL;DR

This paper presents a framework that combines UML-based modelling, large language models, and formal verification to improve requirements engineering and automate parts of the software development process.

Contribution

It introduces a novel integrated approach leveraging LLMs and logical reasoning for UML diagram development, formal verification, and automatic program skeleton generation.

Findings

Enhanced visualisation at various modelling stages

Automated translation of behavioural models into formal specifications

Streamlined transition from design to implementation

Abstract

The requirements engineering (RE) phase is pivotal in developing high-quality software. Integrating advanced modelling techniques with large language models (LLMs) and formal verification in a logical style can significantly enhance this process. We propose a comprehensive framework that focuses on specific Unified Modelling Language (UML) diagrams for preliminary system development. This framework offers visualisations at various modelling stages and seamlessly integrates large language models and logical reasoning engines. The behavioural models generated with the assistance of LLMs are automatically translated into formal logical specifications. Deductive formal verification ensures that logical requirements and interrelations between software artefacts are thoroughly addressed. Ultimately, the framework facilitates the automatic generation of program skeletons, streamlining the transition from design to implementation.