• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Software engineering and formal methods >LTL Model Checking under Fairness in ProB
【24h】

LTL Model Checking under Fairness in ProB

机译：ProB中公平性下的LTL模型检查

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

摘要

Model checking of liveness properties often results in unrealistic, unfair infinite behaviors as counterexamples. Fairness is a notion where the search is constrained to infinite paths that do not ignore infinitely the execution of a set of enabled actions. In this work we present an implementation for efficient checking of LTL formulas under strong and weak fairness in ProB, available for model checking B, Event-B, Z, CSP and CSP||B models. The fairness checking algorithm can cope with both weak and strong fairness conditions, where the respective fairness conditions can be joined by means of the logical operators for conjunction and disjunction, which makes setting up and checking fairness to a property more flexible. We evaluate the implementation on various CSP models and compare it to t he fairness implementation of the PAT tool.
机译：对活动属性进行模型检查通常会导致不现实，不公平的无限行为作为反例。公平是一个概念，其中搜索被限制在无限的路径上，该路径不会无限地忽略一组启用操作的执行。在这项工作中，我们提出了在ProB中强弱条件下有效检查LTL公式的实现，可用于模型检查B，事件B，Z，CSP和CSP || B模型。公平性检查算法可以同时满足弱和强公平性条件，在这种情况下，可以通过逻辑运算符将各个公平性条件结合在一起进行合取和析取，这使得设置和检查属性的公平性更加灵活。我们评估了各种CSP模型的实现，并将其与PAT工具的公平实现进行了比较。

著录项

  • 来源
  • 会议地点 Vienna(AU)
  • 作者

    Ivaylo Dobrikov; Michael Leuschel; Daniel Plagge;

  • 作者单位

    Institut fuer Informatik, Universitaet Duesseldorf, Universitaetsstr. 1, 40225 Duesseldorf, Germany;

    Institut fuer Informatik, Universitaet Duesseldorf, Universitaetsstr. 1, 40225 Duesseldorf, Germany;

    Institut fuer Informatik, Universitaet Duesseldorf, Universitaetsstr. 1, 40225 Duesseldorf, Germany;

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

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号