• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Electronic Notes in Theoretical Computer Science >Model Checking of Component Protocol Conformance – Optimizations by Reducing False Negatives
【24h】

Model Checking of Component Protocol Conformance – Optimizations by Reducing False Negatives

机译：组件协议一致性的模型检查–通过减少错误的否定词进行优化

获取原文
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In past years, a number of works considered behavioral protocols of components and discussed approaches for automatically checking of compatibality of protocols (protocol conformance) in component-based systems. The approaches are usually model-checking approaches, i.e., a positive answer guarantees protocol conformance for all executions while a negative answer provides example executions that may lead to protocol violations. It turned out that if behavioral abstractions take into account unbounded concurrency and unbounded recursion, the protocol conformance checking problem becomes undecidable. There are two possibilities to overcome this problem: (i) further behavioral abstraction to finite state systems or (ii) a conservative approximation of the protocol conformance checking problem. Both approaches may lead tospurious counterexamples, i.e., due to abstractions or approximations the shown execution can never happen. This work considers the second approach and shows a heuristics that reduces the number of spurious counterexamples by cutting off search branches that definitely do not contain real counterexamples.
机译：在过去的几年中，许多工作考虑了组件的行为协议，并讨论了在基于组件的系统中自动检查协议兼容性（协议一致性）的方法。所述方法通常是模型检查方法，即，肯定答案保证所有执行的协议一致性，而否定答案提供可能导致违反协议的示例执行。事实证明，如果行为抽象考虑到无限制的并发和无限制的递归，则协议一致性检查问题将变得不确定。有两种方法可以解决此问题：（i）进一步将行为抽象到有限状态系统，或者（ii）协议一致性检查问题的保守近似。两种方法都可能导致虚假的反例，即由于抽象或近似，所显示的执行永远不会发生。这项工作考虑了第二种方法，并展示了一种启发式方法，该方法可通过切断绝对不包含真实反例的搜索分支来减少虚假反例的数量。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号