Cargando…
SAW: A Tool for Safety Analysis of Weakly-Hard Systems
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 saf...
Autores principales: | , , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363216/ http://dx.doi.org/10.1007/978-3-030-53288-8_26 |
_version_ | 1783559625128280064 |
---|---|
author | Huang, Chao Chang, Kai-Chieh Lin, Chung-Wei Zhu, Qi |
author_facet | Huang, Chao Chang, Kai-Chieh Lin, Chung-Wei Zhu, Qi |
author_sort | Huang, Chao |
collection | PubMed |
description | 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. |
format | Online Article Text |
id | pubmed-7363216 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
record_format | MEDLINE/PubMed |
spelling | pubmed-73632162020-07-16 SAW: A Tool for Safety Analysis of Weakly-Hard Systems Huang, Chao Chang, Kai-Chieh Lin, Chung-Wei Zhu, Qi Computer Aided Verification Article 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. 2020-06-13 /pmc/articles/PMC7363216/ http://dx.doi.org/10.1007/978-3-030-53288-8_26 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. |
spellingShingle | Article Huang, Chao Chang, Kai-Chieh Lin, Chung-Wei Zhu, Qi SAW: A Tool for Safety Analysis of Weakly-Hard Systems |
title | SAW: A Tool for Safety Analysis of Weakly-Hard Systems |
title_full | SAW: A Tool for Safety Analysis of Weakly-Hard Systems |
title_fullStr | SAW: A Tool for Safety Analysis of Weakly-Hard Systems |
title_full_unstemmed | SAW: A Tool for Safety Analysis of Weakly-Hard Systems |
title_short | SAW: A Tool for Safety Analysis of Weakly-Hard Systems |
title_sort | saw: a tool for safety analysis of weakly-hard systems |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363216/ http://dx.doi.org/10.1007/978-3-030-53288-8_26 |
work_keys_str_mv | AT huangchao sawatoolforsafetyanalysisofweaklyhardsystems AT changkaichieh sawatoolforsafetyanalysisofweaklyhardsystems AT linchungwei sawatoolforsafetyanalysisofweaklyhardsystems AT zhuqi sawatoolforsafetyanalysisofweaklyhardsystems |