YI-TING HSIEHChang, Tzu TaoTzu TaoChangTsai, Chen JunChen JunTsaiWu, Shih LunShih LunWuBai, Ching YuanChing YuanBaiChang, Kai ChiehKai ChiehChangCHUNG-WEI LINKang, EunsukEunsukKangHuang, ChaoChaoHuangZhu, QiQiZhu2023-09-012023-09-012023-07-142378962Xhttps://scholars.lib.ntu.edu.tw/handle/123456789/634906A weakly-hard fault model can be captured by an (m,k) constraint, where 0≤ m≤ k, meaning that there are at most m bad events (faults) among any k consecutive events. In this article, 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, then the satisfaction of desired properties is guaranteed; otherwise, the runtime monitor can notify the system to switch to a safe mode. This is especially essential for cyber-physical systems that need to provide guarantees with limited resources and the existence of faults. Experimental results with discrete second-order control, network routing, vehicle following, and lane changing demonstrate the generality and the efficiency of the proposed approaches.Formal verification | runtime monitoring | weakly-hard models[SDGs]SDG11journal article10.1145/36033802-s2.0-85166395100https://api.elsevier.com/content/abstract/scopus_id/85166395100