• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer aided verification >Program Repair without Regret
【24h】

Program Repair without Regret

机译：无遗憾的程序修复

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We present a new and flexible approach to repair reactive programs with respect to a specification. The specification is given in linear-temporal logic. Like in previous approaches, we aim for a repaired program that satisfies the specification and is syntactically close to the faulty program. The novelty of our approach is that it produces a program that is also semantically close to the original program by enforcing that a subset of the original traces is preserved. Intuitively, the faulty program is considered to be a part of the specification, which enables us to synthesize meaningful repairs, even for incomplete specifications. Our approach is based on synthesizing a program with a set of behaviors that stay within a lower and an upper bound. We provide an algorithm to decide if a program is repairable with respect to our new notion, and synthesize a repair if one exists. We analyze several ways to choose the set of traces to leave intact and show the boundaries they impose on repairability. We have evaluated the approach on several examples.
机译：我们提出了一种新的灵活方法来根据规范修复响应式程序。该规范以线性时态逻辑给出。像以前的方法一样，我们的目标是经过修复的程序，该程序可以满足规范并在语法上接近故障程序。我们的方法的新颖性在于，通过强制保留原始迹线的子集，它可以在语义上接近原始程序，从而生成一个程序。直觉上，有故障的程序被视为规范的一部分，这使我们能够合成有意义的维修，即使对于不完整的规范也是如此。我们的方法基于一个程序，该程序具有一组行为，这些行为处于上下限内。我们提供了一种算法，可以根据我们的新概念来确定程序是否可修复，并在存在某个修复程序时对其进行综合。我们分析了几种选择完整迹线的方法，并显示了它们对可修复性的限制。我们已经通过几个示例评估了该方法。

著录项

  • 来源
    《Computer aided verification》|2013年|896-911|共16页
  • 会议地点 Saint Petersburg(RU)
  • 作者

    Christian von Essen; Barbara Jobstmann;

  • 作者单位

    Verimag, CNRS and Universities of Grenoble, France;

    Verimag, CNRS and Universities of Grenoble, France ,Jasper Design Automation, CA ,Ecole Polytechnique Federale de Lausanne, Switzerland;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号