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

doi:10.1007/978-3-030-60508-7_28

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

Electrical and Computer Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 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	https://doi.org/10.1007/978-3-030-60508-7_28
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

Keywords

Formal verification
Weakly-hard models

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-030-60508-7_28

Cite this

Wu, S. L., Bai, C. Y., Chang, K. C., Hsieh, Y. T., Huang, C., Lin, C. W., Kang, E., & Zhu, Q. (2020). Efficient System Verification with Multiple Weakly-Hard Constraints for Runtime Monitoring. In J. Deshmukh, & D. Nickovic (Eds.), Runtime Verification - 20th International Conference, RV 2020, Proceedings (pp. 497-516). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12399 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-60508-7_28

Wu, Shih Lun ; Bai, Ching Yuan ; Chang, Kai Chieh ; Hsieh, Yi Ting ; Huang, Chao ; Lin, Chung Wei ; Kang, Eunsuk ; Zhu, Qi. / Efficient System Verification with Multiple Weakly-Hard Constraints for Runtime Monitoring. Runtime Verification - 20th International Conference, RV 2020, Proceedings. editor / Jyotirmoy Deshmukh ; Dejan Nickovic. Springer Science and Business Media Deutschland GmbH, 2020. pp. 497-516 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e9c4470722284a2580e5978207d1ae70,

title = "Efficient System Verification with Multiple Weakly-Hard Constraints for Runtime Monitoring",

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

keywords = "Formal verification, Weakly-hard models",

author = "Wu, {Shih Lun} and Bai, {Ching Yuan} and Chang, {Kai Chieh} and Hsieh, {Yi Ting} and Chao Huang and Lin, {Chung Wei} and Eunsuk Kang and Qi Zhu",

note = "Funding Information: 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. Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 20th International Conference on Runtime Verification, RV 2020 ; Conference date: 06-10-2020 Through 09-10-2020",

year = "2020",

doi = "10.1007/978-3-030-60508-7_28",

language = "English (US)",

isbn = "9783030605070",

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

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "497--516",

editor = "Jyotirmoy Deshmukh and Dejan Nickovic",

booktitle = "Runtime Verification - 20th International Conference, RV 2020, Proceedings",

address = "Germany",

}

Wu, SL, Bai, CY, Chang, KC, Hsieh, YT, Huang, C, Lin, CW, Kang, E & Zhu, Q 2020, Efficient System Verification with Multiple Weakly-Hard Constraints for Runtime Monitoring. in J Deshmukh & D Nickovic (eds), Runtime Verification - 20th International Conference, RV 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12399 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 497-516, 20th International Conference on Runtime Verification, RV 2020, Los Angeles, United States, 10/6/20. https://doi.org/10.1007/978-3-030-60508-7_28

Efficient System Verification with Multiple Weakly-Hard Constraints for Runtime Monitoring. / Wu, Shih Lun; Bai, Ching Yuan; Chang, Kai Chieh; Hsieh, Yi Ting; Huang, Chao; Lin, Chung Wei; Kang, Eunsuk; Zhu, Qi.

Runtime Verification - 20th International Conference, RV 2020, Proceedings. ed. / Jyotirmoy Deshmukh; Dejan Nickovic. Springer Science and Business Media Deutschland GmbH, 2020. p. 497-516 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12399 LNCS).

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

TY - GEN

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

AU - Wu, Shih Lun

AU - Bai, Ching Yuan

AU - Chang, Kai Chieh

AU - Hsieh, Yi Ting

AU - Huang, Chao

AU - Lin, Chung Wei

AU - Kang, Eunsuk

AU - Zhu, Qi

N1 - Funding Information: 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. Publisher Copyright: © 2020, Springer Nature Switzerland AG.

PY - 2020

Y1 - 2020

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

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

KW - Formal verification

KW - Weakly-hard models

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

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

U2 - 10.1007/978-3-030-60508-7_28

DO - 10.1007/978-3-030-60508-7_28

M3 - Conference contribution

AN - SCOPUS:85093103660

SN - 9783030605070

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

SP - 497

EP - 516

BT - Runtime Verification - 20th International Conference, RV 2020, Proceedings

A2 - Deshmukh, Jyotirmoy

A2 - Nickovic, Dejan

PB - Springer Science and Business Media Deutschland GmbH

T2 - 20th International Conference on Runtime Verification, RV 2020

Y2 - 6 October 2020 through 9 October 2020

ER -

Wu SL, Bai CY, Chang KC, Hsieh YT, Huang C, Lin CW et al. Efficient System Verification with Multiple Weakly-Hard Constraints for Runtime Monitoring. In Deshmukh J, Nickovic D, editors, Runtime Verification - 20th International Conference, RV 2020, Proceedings. Springer Science and Business Media Deutschland GmbH. 2020. p. 497-516. (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-60508-7_28

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

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this