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 language | English (US) |
---|---|
Title of host publication | Runtime Verification - 20th International Conference, RV 2020, Proceedings |
Editors | Jyotirmoy Deshmukh, Dejan Nickovic |
Publisher | Springer Science and Business Media Deutschland GmbH |
Pages | 497-516 |
Number of pages | 20 |
ISBN (Print) | 9783030605070 |
DOIs | |
State | Published - 2020 |
Event | 20th International Conference on Runtime Verification, RV 2020 - Los Angeles, United States Duration: Oct 6 2020 → Oct 9 2020 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 12399 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 20th International Conference on Runtime Verification, RV 2020 |
---|---|
Country/Territory | United States |
City | Los Angeles |
Period | 10/6/20 → 10/9/20 |
Funding
This work is 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-108V0901 and NTU-107V0901, the Taiwan Ministry of Science and Technology (MOST) grants MOST-109-2636-E-002-022 and MOST-108-2636-E-002-011. It is also supported by the National Science Foundation (NSF) awards CCF-1918140, CNS-1834701, CNS-1801546, and the Office of Naval Research (ONR) grant N00014-19-1-2496. Shih-Lun Wu and Ching-Yuan Bai contributed equally.
Keywords
- Formal verification
- Weakly-hard models
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science