...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Theory and Practice of Logic Programming >Constraint-based deadlock checking of high-level specifications
【24h】

Constraint-based deadlock checking of high-level specifications

机译：基于约束的高级规范死锁检查

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

摘要

Establishing the absence of deadlocks is important in many applications of formal methods. The use of model checking for finding deadlocks in formal models is often limited. In this paper, we propose a constraint-based approach to finding deadlocks employing the ProB constraint solver. We present the general technique, as well as various improvements that had to be performed on ProB's Prolog kernel, such as reification of membership and arithmetic constraints. This work was guided by an industrial case study, where a team from Bosch was modelling a cruise control system. Within this case study, ProB was able to quickly find counterexamples to very large deadlock-freedom constraints. In the paper, we also present other successful applications of this new technique. Experiments using SAT and SMT solvers on these constraints were thus far unsuccessful.
机译：在形式方法的许多应用中，确定没有死锁是很重要的。使用模型检查来查找正式模型中的死锁通常受到限制。在本文中，我们提出了一种基于约束的方法，该方法使用ProB约束求解器查找死锁。我们介绍了通用技术以及ProB的Prolog内核必须执行的各种改进，例如成员资格的确定和算术约束。这项工作是在一个工业案例研究的指导下进行的，博世的一个团队正在对一个巡航控制系统进行建模。在此案例研究中，ProB能够快速找到非常大的无死锁约束的反例。在本文中，我们还介绍了这项新技术的其他成功应用。到目前为止，使用SAT和SMT求解器对这些约束进行的实验均未成功。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号