一句话：提出反例引导的归纳修复方法，用于自动修复第三方反应式组件的契约。
在用第三方可执行组件构建控制系统时，组件附带的非形式行为描述往往不够严格，难以支撑系统级验证。本文要求分析者先假设一个组件契约，再检查组件是否满足该契约；若不满足，则通过反例引导的归纳修复技术自动修改契约，使其既强到足以证明系统性质，又弱到能覆盖系统上下文中的潜在行为。初步评估显示：修复后的契约在超过32%的案例中与开发者手工编写的契约逻辑等价；在另外63%的案例中，它是组件的一条不同、有效且非平凡的性质。
Using third-party executable components to build control systems poses challenges for verification. This is because the informal behavior descriptions that typically accompany the components often fall short of the needed rigor. Consequently, there is a need to formalize a component contract that is strong enough to help establish system properties and also weak enough to account for all potential component behaviors in the system’s context. In this paper, we present a novel approach that allows an analyst to hypothesize a component contract, explore if the component meets the contract, and, if not, have automated support to help repair the contract. Preliminary results show that, in more than 32% of the cases, the repaired contract is logically equivalent to a developer-written one; in a further 63% of cases, it is a distinct, valid, and non-trivial property of the component.
DOI 原文 ·
@inproceedings{paperbot6536,
title = {Counterexample Guided Inductive Repair of Reactive Contracts},
author = {Soha Hussein and Vaibhav Sharma and Stephen McCamant and Sanjai Rayadurgam and Mats Heimdahl},
booktitle = {ASE},
year = {2021},
doi = {10.1109/ase51524.2021.9678548}
}