论文标题
SAW：用于安全性系统安全分析的工具
SAW: A Tool for Safety Analysis of Weakly-hard Systems
论文作者
论文摘要
我们介绍了SAW，这是一种用于安全性弱系统安全分析的工具，其中传统的硬时正时限制放宽了，以允许有限的截止日期错过，以提高设计灵活性和运行时的弹性。安全验证是虚弱系统的关键问题，因为它可以确保在允许的截止日期内确保系统安全。以前的工作仅用于线性系统，或仅限于某种类型的非线性系统（例如，满足指数稳定性和LIPSCHITZ连续性的系统）。在这项工作中，我们提出了一种新技术，用于对一般非线性弱弱系统的无限时间安全验证。我们的方法首先将设置的安全状态离散到网格中，并构建有向图，其中节点代表网格和边缘代表可及性关系。基于图理论和动态编程，我们的方法可以有效地找到安全的初始集合（由一组网格组成），在给定的弱限制下，可以从中证明系统可以安全。实验结果证明了与最先进的方法相比，我们的方法的有效性。我们的工具的开源实现可在https://github.com/551100kk/saw上获得。可以在https://www.csie.du.edu.tw/~r08922054/saw.ova上找到该工具准备运行的虚拟机。
We introduce SAW, a tool for safety analysis of weakly-hard systems, in which traditional hard timing constraints are relaxed to allow bounded deadline misses for improving design flexibility and runtime resiliency. Safety verification is a key issue for weakly-hard systems, as it ensures system safety under allowed deadline misses. Previous works are either for linear systems only, or limited to a certain type of nonlinear systems (e.g., systems that satisfy exponential stability and Lipschitz continuity of the system dynamics). In this work, we propose a new technique for infinite-time safety verification of general nonlinear weakly-hard systems. Our approach first discretizes the safe state set into grids and constructs a directed graph, where nodes represent the grids and edges represent the reachability relation. Based on graph theory and dynamic programming, our approach can effectively find the safe initial set (consisting of a set of grids), from which the system can be proven safe under given weakly-hard constraints. Experimental results demonstrate the effectiveness of our approach, when compared with the state-of-the-art. An open source implementation of our tool is available at https://github.com/551100kk/SAW. The virtual machine where the tool is ready to run can be found at https://www.csie.ntu.edu.tw/~r08922054/SAW.ova.
