• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Integrated formal methods >Automatic Verification of Parametric Specifications with Complex Topologies
【24h】

Automatic Verification of Parametric Specifications with Complex Topologies

机译：自动验证具有复杂拓扑的参数规范

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

摘要

The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.
机译：本文的重点是通过在各个级别上利用模块性来降低验证的复杂性：规范，验证和结构。对于规范，我们使用模块化语言CSP-OZ-DC，这使我们能够将与数据有关的验证任务与与持续时间有关的任务分离。在验证级别，我们利用定理证明中的模块化来获取丰富的数据结构，并将其用于不变性检查。在结构层次上，我们分析了由相互作用的各种组件组成的系统的模块化验证的可能性。我们通过自动验证来自欧洲火车控制系统标准的案例研究的安全属性来说明这些想法，该案例研究通过包含具有轨道段和具有不同路线的火车列表的复杂轨道拓扑，扩展了先前的示例。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号