• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Symposium on Model-Based Safety and Assessment >On Efficiently Specifying Models for Model Checking
【24h】

On Efficiently Specifying Models for Model Checking

机译：有效地指定模型检查模型

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

摘要

Using formal methods for quality assurance is recommended in many standards for safety critical applications. In most industrial contexts, model checking is the only viable option for formal verification, as interactive approaches often require very highly specialized experts. However, model checking typically suffers from the well-known state-space explosion problem. Due to this problem, engineers typically have to decide on a trade-off between readability and completeness of the model on one side, and the state space size, and thus, computational feasibility on the other. In this paper, we propose a method for reducing the state space by restructuring models. The core idea is to introduce as few additional states as possible by model design making state transitions more complex. To avoid unreadability and infeasible model sizes, we introduce a concept for hierarchical boolean formulas to efficiently specify state transitions. For evaluation purposes, we applied this approach to a case study using the VECS toolkit. In this exemplary case study, we were able to reduce the state space size significantly and make verification time feasible.
机译：建议使用正式保证质量保证，以便在许多安全关键型应用标准中。在大多数工业背景下，模型检查是正式验证的唯一可行的选择，因为互动方法通常需要非常高度专业的专家。然而，模型检查通常存在着名的状态空间爆炸问题。由于这个问题，工程师通常必须决定在一侧模型的可读性和完整性之间的权衡，以及状态空间大小，因此对另一方的计算可行性。在本文中，我们提出了一种通过重组模型来减少状态空间的方法。核心思想是通过模型设计制作状态转换更复杂地介绍尽可能少的其他状态。为避免不可变和不可行的模型大小，我们向分层布尔公式介绍了一个概念，以有效地指定状态转换。为了评估目的，我们将这种方法应用于使用VECS工具包的案例研究。在这种示例性研究中，我们能够显着降低状态空间大小并进行验证时间可行。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号