Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Michal Töpfer, František Plášil, Tomáš Bureš, Petr Hnětynka

TL;DR

This paper shows 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, and specifies these as constraints in a novel temporal logic FCL that allows the behavior of traces with much finer granularity than classical LTL enables.

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.

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

TL;DR

This paper shows 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, and specifies these as constraints in a novel temporal logic FCL that allows the behavior of traces with much finer granularity than classical LTL enables.

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.
Paper Structure (41 sections, 11 equations, 4 figures)

This paper contains 41 sections, 11 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Background and Running Example
  3. Running example
  4. Modeling the running example as a CAS
  5. Vibe Coding and Feedback Verification
  6. Combining adaptation and feedback loops
  7. Prompt generation
  8. Domain description
  9. Architecture specification
  10. Prompt content
  11. Verification of the AM in system runs
  12. Functional Constraints Logic (FCL)
  13. FCL syntax and semantics
  14. Examples of functional constraints for Dragon Hunt in FCL
  15. The game is won
  16. ...and 26 more sections

Figures (4)

  • Figure 1: Combining adaptation and feedback loops.
  • Figure 2: Distributions of the number of feedback-loop iterations needed to obtain a valid AM in Dragon Hunt example. Bars show counts over 10 experiments for each variant.
  • Figure 3: Distributions of the number of feedback-loop iterations needed to obtain a valid AM in Smart Farm example. Bars show counts over 10 independent experiments for each variant.
  • Figure 4: Two runs of an experiment -- one successful (valid AM after 3 iterations) and one reaching a dead end and not improving anymore.