Wu S.-LBai C.-YChang K.-CHsieh Y.-THuang CCHUNG-WEI LINKang EZhu Q.2023-06-092023-06-0920203029743https://www.scopus.com/inward/record.uri?eid=2-s2.0-85093103660&doi=10.1007%2f978-3-030-60508-7_28&partnerID=40&md5=c6d5b893e64f517180072123c5d66618https://scholars.lib.ntu.edu.tw/handle/123456789/632557A 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. © 2020, Springer Nature Switzerland AG.Formal verification; Weakly-hard modelsComputer science; Computers; Hard constraints; Hard faults; Runtime Monitoring; Runtime monitors; Second orders; System environment; System verifications; Artificial intelligenceconference paper10.1007/978-3-030-60508-7_282-s2.0-85093103660