发表机构
Imperial College London; Universidad de Buenos Aires; CONICET; Universidad de San Andrés（帝国理工学院; 布宜诺斯艾利斯大学; 阿根廷国家科学与技术研究理事会; 圣安德烈斯大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对GR(1)规范在环境假设违反时系统保证失效的问题，提出基于预言引导归纳综合的规范调整方法，通过最小化降级系统保证以维持可实现性，并在案例中保留全部原始保证。
AI 中文摘要
反应式综合是一种强大的工具，能够从形式化规范中生成正确性由构造保证的控制器。GR(1)是一种假设-保证规范框架，支持高效的综合，使得综合出的控制器能够广泛应用于各类场景。此类控制器的局限性在于，一旦遇到规范假设中未指定的环境行为，系统保证将不再成立。我们的工作提出了一种基于预言引导的归纳综合的方法，用于调整规范以使其与观察到的假设违反保持一致，同时尽可能少地降级系统保证以维持可实现性。我们的方法能够发现多个潜在解决方案，因此我们提出了一种偏好标准，该标准基于规范在适应过程中支持鲁棒性的能力。尽管我们的方法能够降级整个规范，但在我们的案例研究中，我们成功发现了能够保留全部原始保证集的降级方案。
英文摘要
Reactive synthesis is a powerful tool for generating correct-by-construction controllers from formal specifications. GR(1) is an assume-guarantee specification framework that enables efficient synthesis, allowing synthesised controllers to be used in a wide array of applications. The limitation of such controllers is that, should they encounter environment behaviour unspecified in the assumptions of the specification, the specified system guarantees are no longer ensured. Our work proposes an approach based on oracle-guided inductive synthesis to adapt the specification to be consistent with the observed assumption violation, while degrading system guarantees as little as possible to maintain realisability. Our methodology discovers multiple potential solutions, so we propose a preference criteria, based on the ability of the specification to enable robustness under adaptation. Although our approach is capable of degrading the entire specification, for our case studies we successfully discover degradations that preserve the entire set of original guarantees.
Comments59 pages (39 pages main text, 20 pages appendices), 24 figures, 5 tables. Submitted to ACM Transactions on Software Engineering and Methodology
