Computer Science Department
School of Computer Science, Carnegie Mellon University


ModelPlex: Verified Runtime Validation of
Verified Cyber-Physical System Models

Stefan Mitsch, André Platzer

July 2014


A conference version of this report has appeared at RV 2014 [22].
Stefan Mitsch and André Platzer. ModelPlex: Verified runtime validation of verified cyber-physical system models.
In Borzoo Bonakdarpour and Scott A. Smolka, editors,
Runtime Verification - 5th International Conference, RV 2014, Toronto, Canada, September 22-25, 2014.
Proceedings, volume 8734 of LNCS, pages 199-214. Springer, 2014.

Keywords: Runtime verification, cyber-physical systems, hybrid systems, logic

Formal verification and validation play a crucial role in making cyber-physical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified w.r.t. the model. Otherwise, all bets are off. This paper introduces ModelPlex, a method ensuring that verification results about models apply to CPS implementations. ModelPlex provides correctness guarantees for CPS executions at runtime: it combines offline verification of CPS models with runtime validation of system executions for compliance with the model. Model- Plex 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 so that offline verification results no longer apply, ModelPlex initiates provably safe fallback actions. This paper, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic.

32 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by