Testing learning-enabled cyber-physical systems with Large-Language Models: A Formal Approach

TL;DR

This paper explores the challenges of formally verifying learning-enabled cyber-physical systems and proposes a roadmap to enhance testing methods for formal safety guarantees using Large-Language Models.

Contribution

It identifies key challenges in formal safety verification of ML-integrated CPS and suggests a transition from probabilistic testing to rigorous formal assurance methods.

Findings

Current testing methods are insufficient for formal safety guarantees.

A roadmap is proposed to improve testing with Large-Language Models.

The approach aims to bridge the gap between probabilistic testing and formal verification.

Abstract

The integration of machine learning (ML) into cyber-physical systems (CPS) offers significant benefits, including enhanced efficiency, predictive capabilities, real-time responsiveness, and the enabling of autonomous operations. This convergence has accelerated the development and deployment of a range of real-world applications, such as autonomous vehicles, delivery drones, service robots, and telemedicine procedures. However, the software development life cycle (SDLC) for AI-infused CPS diverges significantly from traditional approaches, featuring data and learning as two critical components. Existing verification and validation techniques are often inadequate for these new paradigms. In this study, we pinpoint the main challenges in ensuring formal safety for learningenabled CPS.We begin by examining testing as the most pragmatic method for verification and validation, summarizing the current state-of-the-art methodologies. Recognizing the limitations in current testing approaches to provide formal safety guarantees, we propose a roadmap to transition from foundational probabilistic testing to a more rigorous approach capable of delivering formal assurance.