• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Software and systems modeling >Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods
【24h】

Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods

机译：通过结合不同的封闭方法，改进SAT模ODE方法以进行混合系统分析

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

摘要

Aiming at automatic verification and analysis techniques for hybrid discrete-continuous systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for large Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODE-LP, as a state-of-the-art interval solver for ODEs, and with bracketing systems, which exploit monotonicity properties allowing to find enclosures for problems that VNODE-LP alone cannot enclose tightly. We apply the combined iSAT-ODE solver to the analysis of a variety of non-linear hybrid systems by solving predicative encodings of reachability properties and of an inductive stability argument, and evaluate the impact of the different enclosure methods, decision heuristics and their combination. Our experiments include classic benchmarks from the literature, as well as a newly-designed conveyor belt system that combines hybrid behavior of parallel components, a slip-stick friction model with non-linear dynamics and flow invariants and several dimensions of parameterization. In the paper, we also present and evaluate an extension of VNODE-LP tailored to its use as a deduction mechanism within iSAT-ODE, to allow fast re-evaluations of enclosures over arbitrary subranges of the analyzed time span.
机译：针对混合离散连续系统的自动验证和分析技术，我们提出了一种将常微分方程（ODE）的封闭方法与iSAT求解器的新颖组合，用于算术约束的大布尔组合。在改进我们之前的工作的基础上，本文的贡献在于将iSAT与VODE-LP（作为ODE的最先进的间隔求解器）相结合，并与利用单调性允许查找问题所在的包围系统相结合。单独的VNODE-LP不能紧密密封。通过求解可达性属性和归纳稳定性参数的预测编码，我们将组合的iSAT-ODE求解器应用于各种非线性混合系统的分析，并评估不同封闭方法，决策启发式方法及其组合的影响。我们的实验包括文献中的经典基准，以及新设计的传送带系统，该系统结合了并行组件的混合行为，具有非线性动力学和流量不变性的滑杆摩擦模型以及多个参数化维度。在本文中，我们还介绍并评估了VNODE-LP的扩展，该扩展量身定制，可作为iSAT-ODE中的推论机制使用，以允许在分析时间跨度的任意子范围内快速重新评估机柜。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号