SAW: A Tool for Safety Analysis of Weakly-Hard Systems

Chao Huang; Kai Chieh Chang; Chung Wei Lin; Qi Zhu

doi:10.1007/978-3-030-53288-8_26

SAW: A Tool for Safety Analysis of Weakly-Hard Systems

Chao Huang^*, Kai Chieh Chang, Chung Wei Lin, Qi Zhu

^*Corresponding author for this work

Electrical and Computer Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

7 Scopus citations

Abstract

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.

Original language	English (US)
Title of host publication	Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
Editors	Shuvendu K. Lahiri, Chao Wang
Publisher	Springer
Pages	543-555
Number of pages	13
ISBN (Print)	9783030532871
DOIs	https://doi.org/10.1007/978-3-030-53288-8_26
State	Published - 2020
Event	32nd International Conference on Computer Aided Verification, CAV 2020 - Los Angeles, United States Duration: Jul 21 2020 → Jul 24 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12224 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	32nd International Conference on Computer Aided Verification, CAV 2020
Country/Territory	United States
City	Los Angeles
Period	7/21/20 → 7/24/20

Keywords

Graph theory
Safety verification
Weakly-hard systems

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-030-53288-8_26

Cite this

Huang, C., Chang, K. C., Lin, C. W., & Zhu, Q. (2020). SAW: A Tool for Safety Analysis of Weakly-Hard Systems. In S. K. Lahiri, & C. Wang (Eds.), Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings (pp. 543-555). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12224 LNCS). Springer. https://doi.org/10.1007/978-3-030-53288-8_26

Huang, Chao ; Chang, Kai Chieh ; Lin, Chung Wei et al. / SAW : A Tool for Safety Analysis of Weakly-Hard Systems. Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. editor / Shuvendu K. Lahiri ; Chao Wang. Springer, 2020. pp. 543-555 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{c90e187a10cc4a42abebe3ba961859ee,

title = "SAW: A Tool for Safety Analysis of Weakly-Hard Systems",

abstract = "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.",

keywords = "Graph theory, Safety verification, Weakly-hard systems",

author = "Chao Huang and Chang, {Kai Chieh} and Lin, {Chung Wei} and Qi Zhu",

note = "Funding Information: This work is supported by the National Science Foundation awards 1834701, 1834324, 1839511, 1724341, and the Office of Naval Research grant N00014-19-1-2496. It is also supported by the Asian Office of Aerospace Research and Development (AOARD), jointly with the Office of Naval Research Global (ONRG), award FA2386-19-1-4037, the Taiwan Ministry of Education (MOE) grants NTU-107V0901 and NTU-108V0901, the Taiwan Ministry of Science and Technology (MOST) grants MOST-108-2636-E-002-011 and MOST-109-2636-E-002-022. Publisher Copyright: {\textcopyright} 2020, The Author(s).; 32nd International Conference on Computer Aided Verification, CAV 2020 ; Conference date: 21-07-2020 Through 24-07-2020",

year = "2020",

doi = "10.1007/978-3-030-53288-8_26",

language = "English (US)",

isbn = "9783030532871",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "543--555",

editor = "Lahiri, {Shuvendu K.} and Chao Wang",

booktitle = "Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings",

}

Huang, C, Chang, KC, Lin, CW & Zhu, Q 2020, SAW: A Tool for Safety Analysis of Weakly-Hard Systems. in SK Lahiri & C Wang (eds), Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12224 LNCS, Springer, pp. 543-555, 32nd International Conference on Computer Aided Verification, CAV 2020, Los Angeles, United States, 7/21/20. https://doi.org/10.1007/978-3-030-53288-8_26

SAW : A Tool for Safety Analysis of Weakly-Hard Systems. / Huang, Chao; Chang, Kai Chieh; Lin, Chung Wei et al.

Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. ed. / Shuvendu K. Lahiri; Chao Wang. Springer, 2020. p. 543-555 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12224 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - SAW

T2 - 32nd International Conference on Computer Aided Verification, CAV 2020

AU - Huang, Chao

AU - Chang, Kai Chieh

AU - Lin, Chung Wei

AU - Zhu, Qi

N1 - Funding Information: This work is supported by the National Science Foundation awards 1834701, 1834324, 1839511, 1724341, and the Office of Naval Research grant N00014-19-1-2496. It is also supported by the Asian Office of Aerospace Research and Development (AOARD), jointly with the Office of Naval Research Global (ONRG), award FA2386-19-1-4037, the Taiwan Ministry of Education (MOE) grants NTU-107V0901 and NTU-108V0901, the Taiwan Ministry of Science and Technology (MOST) grants MOST-108-2636-E-002-011 and MOST-109-2636-E-002-022. Publisher Copyright: © 2020, The Author(s).

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

KW - Graph theory

KW - Safety verification

KW - Weakly-hard systems

UR - http://www.scopus.com/inward/record.url?scp=85089226053&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85089226053&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-53288-8_26

DO - 10.1007/978-3-030-53288-8_26

M3 - Conference contribution

AN - SCOPUS:85089226053

SN - 9783030532871

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 543

EP - 555

BT - Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings

A2 - Lahiri, Shuvendu K.

A2 - Wang, Chao

PB - Springer

Y2 - 21 July 2020 through 24 July 2020

ER -

Huang C, Chang KC, Lin CW, Zhu Q. SAW: A Tool for Safety Analysis of Weakly-Hard Systems. In Lahiri SK, Wang C, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. Springer. 2020. p. 543-555. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-53288-8_26

SAW: A Tool for Safety Analysis of Weakly-Hard Systems

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this