Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logic

TL;DR

This paper presents a novel approach for verifying and generating adaptation managers in CAS systems using vibe coding feedback loops and a new temporal logic FCL for precise requirement specification, demonstrating effective results with minimal iterations.

Contribution

It introduces a new temporal logic FCL for detailed behavior specification and demonstrates the viability of vibe coding feedback loops for generating verified adaptation managers in CAS.

Findings

Few feedback iterations needed for effective verification.

High path coverage achieved in experiments.

Successful application to two CAS domain systems.

Abstract

In CAS adaptation, a challenge is to define the dynamic architecture of the system and changes in its behavior. Implementation-wise, this is projected into an adaptation mechanism, typically realized as an Adaptation Manager (AM). With the advances of generative LLMs, generating AM code based on system specification and desired AM behavior (partially in natural language) is a tempting opportunity. The recent introduction of vibe coding suggests a way to target the problem of the correctness of generated code by iterative testing and vibe coding feedback loops instead of direct code inspection. In this paper, we show that generating an AM via vibe coding feedback loops is a viable option when the verification of the generated AM is based on a very precise formulation of the functional requirements. We specify these as constraints in a novel temporal logic FCL that allows us to express the behavior of traces with much finer granularity than classical LTL enables. Furthermore, we show that by combining the adaptation and vibe coding feedback loops where the FCL constraints are evaluated for the current system state, we achieved good results in the experiments with generating AMs for two example systems from the CAS domain. Typically, just a few feedback loop iterations were necessary, each feeding the LLM with reports describing detailed violations of the constraints. This AM testing was combined with high run path coverage achieved by different initial settings.