SAW：一种用于弱硬系统安全分析的工具
系统与控制
2020-05-15 v1 系统与控制
摘要
我们介绍 SAW，一种用于弱硬系统安全分析的工具，其中传统的硬时序约束被放宽以允许有界截止期限缺失，从而提高设计灵活性和运行时弹性。安全验证是弱硬系统的关键问题，因为它在允许的截止期限缺失下确保系统安全。以往的工作要么仅适用于线性系统，要么局限于某类非线性系统（例如，满足指数稳定性和系统动力学 Lipschitz 连续性的系统）。在这项工作中，我们提出了一种用于一般非线性弱硬系统无限时间安全验证的新技术。我们的方法首先将安全状态集离散化为网格并构建有向图，其中节点表示网格，边表示可达关系。基于图论和动态规划，我们的方法能有效找到安全初始集（由一组网格组成），从中可证明系统在给定弱硬约束下是安全的。实验结果表明，与最先进方法相比，我们的方法有效。我们工具的开源实现可在 https://github.com/551100kk/SAW 获取。工具就绪运行的虚拟机可在 https://www.csie.ntu.edu.tw/~r08922054/SAW.ova 找到。
引用
@article{arxiv.2005.07159,
title = {SAW: A Tool for Safety Analysis of Weakly-hard Systems},
author = {Chao Huang and Kai-Chieh Chang and Chung-Wei Lin and Qi Zhu},
journal= {arXiv preprint arXiv:2005.07159},
year = {2020}
}
备注
Accepted by 32nd International Conference on Computer-Aided Verification (CAV2020)