基于约束逻辑的CAS适应 vibe 编码中的反馈自动验证

在CAS适应中，一个挑战是定义系统的动态架构以及其行为的变化。从实现角度看，这被投射到适应机制中，通常实现为适应经理(AM)。随着生成式LLM的进步，基于系统规范和期望AM行为(部分以自然语言表示)生成AM代码是一个引人入胜的机会。最近引入的vibe编码建议通过迭代测试和vibe编码反馈循环来解决生成代码正确性的问题，而非直接代码检查。在本文中，我们展示，通过vibe编码反馈循环生成AM是一种可行选项，当AM的验证基于非常精确的功能需求形式化表达时。我们将这些需求指定为约束，采用一种新型时序逻辑FCL，该逻辑允许我们比经典LTL更细粒度地表达轨迹的行为。此外，我们表明，通过将适应和vibe编码反馈循环结合起来，其中FCL约束用于评估当前系统状态，我们在两个来自CAS领域的示例系统的实验中取得了良好结果。通常，只需数次反馈循环迭代，每次都为LLM提供描述FCL约束违规的详细报告。这种AM测试与通过不同初始设置实现的高运行路径覆盖率相结合。