A method for ensuring that verification results about models apply to cyber-physical systems (CPS) implementations is presented. The invention provides correctness guarantees for CPS executions at runtime. Offline verification of CPS models are combined with runtime validation of system executions for compliance with the model. The invention ensures that the verification results obtained for the model apply to the actual system runs by monitoring the behavior of the world for compliance with the model, assuming the system dynamics deviation is bounded. If, at some point, the observed behavior no longer complies with the model, such that offline verification results no longer apply, provably safe fallback actions are initiated. The invention includes a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic.
展开▼
