# US 10,872,187 B2 · Verified runtime validation of verified cyber-physical system models > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 10,872,187 B2 - Document ID: US10872187B2 - Status: Granted - Kind: B2 - Application number: 15/026,690 - Filed: 2014-10-10 - Published: 2016-09-01 - Granted: 2020-12-22 - Earliest claimed: 2013-10-11 - Assignees: Carnegie Mellon University - Applicants: Carnegie Mellon University - Inventors: André Platzer; Stefan Mitsch - Web page: https://patentgrep.com/patent/US10872187B2 ## CPC - G06F 30/3323: using formal methods, e.g. equivalence checking or property checking - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) ## Abstract 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. ## Claims ### Claim 1 A computer-implemented method for synthesizing a monitor for a cyber-physical system (CPS) from a verified model of the CPS, the verified model expressed as a set of mathematical formulas, comprising the steps of: deriving a monitor specification from the verified model, the monitor specification comprising a set of specification conjectures, each specification conjecture derived from one of the set of mathematical formulas by verified transformation such that each specification conjecture is satisfied over states of the CPS only if the states are compatible with behavior of the verified model; applying a theorem prover to each specification conjecture to derive one or more monitor conditions expressed as first-order logic by performing logical transformations that successively simplify formulas into structurally simpler formulas expressing effects of the verified model behavior; synthesizing the monitor by syntactic transformation or compilation of the monitor conditions to executable code that verifies the monitor conditions; and verifying the behavior of the CPS by executing the monitor to determine that the CPS meets the set of monitor conditions indicating compliance with the verified model; wherein the CPS includes a controller running control software, the controller reading sensors and controlling actuators, and wherein the monitor verifies the actions of the controller and resulting changes in a state of the CPS. ### Claim 2 (depends on 1) The method of claim 1 further comprising the step of executing the monitor in conjunction with the control software, to guarantee compliance of the CPS with the verified model. ### Claim 3 (depends on 1) The method of claim 1 where the monitor consists of a model monitor, a controller monitor and a prediction monitor. ### Claim 4 (depends on 3) The method of claim 3 wherein the model monitor compares a current state of the CPS with a previous state of he CPS and determines if any differences between the current state and the previous state are in compliance with the verified model. ### Claim 5 (depends on 3) The method of claim 3 wherein the controller monitor monitors the controller to check compliance with the verified model. ### Claim 6 (depends on 3) The method of claim 3 wherein the prediction monitor allows deviations of the cyber-physical system from the verified model to account for real-world imperfections. ### Claim 7 (depends on 4) The method of claim 4 wherein the model monitor, the controller monitor and the prediction monitor read the sensors to determine the current state of the CPS. ### Claim 8 (depends on 7) The method of claim 7 wherein the model monitor runs prior to the control software and determines if physical behavior which occurred between the previous state and the current state is in compliance with the verified model. ### Claim 9 (depends on 8) The method of claim 8 wherein the model monitor will raise an error if any differences between the current state and the previous state are not in compliance with the verified model. ### Claim 10 (depends on 5) The method of claim 5 wherein the controller monitor runs after the control software and determines if physical actions to be taken by the controller will result in the CPS being in compliance with the verified model. ### Claim 11 (depends on 10) The method of claim 10 wherein the controller monitor will raise an error if the physical actions will result in the CPS not being in compliance with the verified model. ### Claim 12 (depends on 6) The method of claim 6 wherein the prediction monitor runs after the control software and determines if physical actions to be taken by the controller will result in the CPS being in compliance with the verified model in the presence of bounded deviations between the CPS and the verified model. ### Claim 13 (depends on 12) The method of claim 12 wherein the prediction monitor will raise an error if the physical actions to be taken by the controller will result in the CPS not being in compliance with the verified model. ### Claim 14 (depends on 1) The method of claim 1 wherein the verified model comprises a set of formulas of the form: Φ→[α*]ψ with invariant ψ→[α]ψ s.t. Φ→φ and φ→ψ (1) where: Φ is a precondition for the run; α* describes repeated runs of the hybrid system; α is the hybrid system model; ψ is a postcondition for the run; and φ is a loop invariant. ### Claim 15 (depends on 8) The method of claim 8 wherein compliance with the model monitor guarantees that properties of the verified model are present in the CPS before the control software is executed. ### Claim 16 (depends on 10) The method of claim 10 wherein compliance with the controller monitor guarantees that properties of the verified model are present in the CPS after the control software is executed. ### Claim 17 (depends on 12) The method of claim 12 wherein compliance with the prediction monitor guarantees that properties of the verified model will still be present in future states of the CPS. ### Claim 18 (depends on 1) The method of claim 1 wherein the method is automated in accordance with an algorithm. ### Claim 19 (depends on 1) The method of claim 1 wherein the mathematical formulas are differential dynamic logic formulas. ### Claim 20 (depends on 3) The method of claim 3, wherein the prediction monitor predicts a next state of the CPS based on the actions to be taken by the controller and initiates failsafe actions if the next state of the CPS deviates from the verified model.