Efficient System Verification with Multiple Weakly-Hard Constraints for Runtime Monitoring

Shih Lun Wu, Ching Yuan Bai, Kai Chieh Chang, Yi Ting Hsieh, Chao Huang, Chung Wei Lin*, Eunsuk Kang, Qi Zhu

*Corresponding author for this work

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

Abstract

A weakly-hard fault model can be captured by an (m, k) constraint, where (Formula Presented), meaning that there are at most m bad events (faults) among any k consecutive events. In this paper, we use a weakly-hard fault model to constrain the occurrences of faults in system inputs. We develop approaches to verify properties for all possible values of (m, k), where k is smaller than or equal to a given K, in an exact and efficient manner. By verifying all possible values of (m, k), we define weakly-hard requirements for the system environment and design a runtime monitor based on counting the number of faults in system inputs. If the system environment satisfies the weakly-hard requirements, the satisfaction of desired properties is guaranteed; otherwise, the runtime monitor can notify the system to switch to a safe mode. Experimental results with a discrete second-order controller demonstrate the efficiency of the proposed approaches.

Original languageEnglish (US)
Title of host publicationRuntime Verification - 20th International Conference, RV 2020, Proceedings
EditorsJyotirmoy Deshmukh, Dejan Nickovic
PublisherSpringer Science and Business Media Deutschland GmbH
Pages497-516
Number of pages20
ISBN (Print)9783030605070
DOIs
StatePublished - 2020
Event20th International Conference on Runtime Verification, RV 2020 - Los Angeles, United States
Duration: Oct 6 2020Oct 9 2020

Publication series

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

Conference

Conference20th International Conference on Runtime Verification, RV 2020
Country/TerritoryUnited States
CityLos Angeles
Period10/6/2010/9/20

Keywords

  • Formal verification
  • Weakly-hard models

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Efficient System Verification with Multiple Weakly-Hard Constraints for Runtime Monitoring'. Together they form a unique fingerprint.

Cite this