Treffer: Model Predictive Runtime Verification for Cyber-Physical Systems with Real-Time Deadlines

Cyber-physical systems often require fault detection of future events in order to mitigate the fault before failure occurs. Effective on-board runtime verification (RV) will need to not only determine the system’s current state but also predict future faults by predetermined mitigation trigger deadlines. For example, if it takes three seconds to deploy the parachute of an Unmanned Aerial System (UAS), the deployment of the parachute must be triggered three seconds before it is needed to mitigate the impending crash. To allow for the detection of future faults by deadlines, we design a real-time Model Predictive Runtime Verification (MPRV) algorithm that uniquely uses current data traces whenever possible, predicting only the minimum horizon needed to make an on-deadline evaluation. AlthoughMPRV is extensible to other RV engines, we deploy the algorithm on the R2U2 RV engine due to R2U2’s resource-aware architecture, real-time guarantees, and deployment history.We demonstrate the utility of theMPRV algorithm through a quadcopter case study and evaluate the effectiveness of our implementation by conducting memory usage and runtime performance analysis in a resource-constrained FPGA environment. ; This is a manuscript of a proceeding published as Zhang, Pei, Alexis Aurandt, Rohit Dureja, Phillip H. Jones, and Kristin Yvonne Rozier. "Model Predictive Runtime Verification for Cyber-Physical Systems with Real-Time Deadlines." In International Conference on Formal Modeling and Analysis of Timed Systems, pp. 158-180. Cham: Springer Nature Switzerland, 2023. doi: https://doi.org/10.1007/978-3-031-42626-1_10.