System Verification and Runtime Monitoring with Multiple Weakly-Hard Constraints

Hsieh, Yi-Ting, Chang, Tzu-Tao, Tsai, Chen-Jun, Wu, Shih-Lun, Bai, Ching-Yuan, Chang, Kai-Chieh, Lin, Chung-Wei, Kang, Eunsuk, Huang, Chao ORCID: 0000-0002-9300-1787 and Zhu, Qi (2023) System Verification and Runtime Monitoring with Multiple Weakly-Hard Constraints. ACM TRANSACTIONS ON CYBER-PHYSICAL SYSTEMS, 7 (3). pp. 1-28.

PDF
System_Verification_and_Runtime_Monitoring_with_Multiple_Weakly_Hard_Constraints.pdf - Author Accepted Manuscript
Download (934kB) | Preview

Official URL: http://dx.doi.org/10.1145/3603380

Abstract

<jats:p> A weakly-hard fault model can be captured by an <jats:italic>(m,k)</jats:italic> constraint, where 0≤ <jats:italic>m</jats:italic> ≤ <jats:italic>k</jats:italic> , meaning that there are at most <jats:italic>m</jats:italic> bad events (faults) among any <jats:italic>k</jats:italic> 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 <jats:italic>(m,k)</jats:italic> , where <jats:italic>k</jats:italic> is smaller than or equal to a given <jats:italic>K</jats:italic> , in an exact and efficient manner. By verifying all possible values of <jats:italic>(m,k)</jats:italic> , 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. </jats:p>

Item Type:	Article
Uncontrolled Keywords:	Formal verification, runtime monitoring, weakly-hard models
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	18 Jul 2023 08:14
Last Modified:	23 Aug 2023 13:58
DOI:	10.1145/3603380
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3171718