Runtime model validation for partially-observable hybrid systems
AssigneeCarnegie Mellon University
InventorsStefan Mitsch, Andre Platzer
Life of this patent
Estimating the term…
Abstract
Disclosed herein are techniques to make the synthesized monitoring conditions of partially-observable hybrid systems robust to partial observability of sensor uncertainty and partial controllability due to actuator disturbance. The approach herein shows that the monitoring conditions result in provable safety guarantees with fallback controllers that react to monitor violation at runtime.
Claims31
A process for verifying compliance of a partially observable cyber-physical system (CPS) with a proven hybrid model of the CPS, the hybrid model describing a desired behavior of the CPS with both observable and unobservable variables, comprising the steps of:
- deriving a monitor specification from the hybrid model in differential dynamic logic, the monitor specification comprising a set of logical constraints regarding behavior of the model;
- obtaining consecutive sensor measurements from one or more sensors measuring one or more observable quantities during operation of the CPS;
- determining a monitor verdict, using the monitor specification, the monitor verdict indicating success if prior measurements of the one or more observable quantities are predictive of future measurements of the one or more observable quantities and one or more inferred unobservable quantities within an acceptable measurement uncertainty, and, indicating failure otherwise;
- wherein a successful monitor verdict guarantees safety of the CPS and compliance of the observable and unobservable true behavior of the CPS with the hybrid model;
- and
- engaging a fallback action of the CPS when the monitor verdict indicates failure.
Dependencies are inferred from the claim text.