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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish (US)
Title of host publicationComputer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
EditorsShuvendu K. Lahiri, Chao Wang
PublisherSpringer
Pages543-555
Number of pages13
ISBN (Print)9783030532871
DOIs
StatePublished - 2020
Event32nd International Conference on Computer Aided Verification, CAV 2020 - Los Angeles, United States
Duration: Jul 21 2020Jul 24 2020

Publication series

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

Conference

Conference32nd International Conference on Computer Aided Verification, CAV 2020
CountryUnited States
CityLos Angeles
Period7/21/207/24/20

Keywords

  • Graph theory
  • Safety verification
  • Weakly-hard systems

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'SAW: A Tool for Safety Analysis of Weakly-Hard Systems'. Together they form a unique fingerprint.

Cite this