Go to page
 

Bibliographic Metadata

Title
ModelPlex : verified runtime validation of verified cyber-physical system models
AuthorMitsch, Stefan ; Platzer, André
Published in
Formal Methods in System Design, 2016, Vol. 49, Issue 1-2, page 33-74
PublishedSpringer, 2016
LanguageEnglish
Document typeJournal Article
Keywords (EN)Runtime verification / Static verification / Cyber-physical systems / Hybrid systems / Differential dynamic logic
Project-/ReportnumberDARPA FA8750-12-2-0291
Project-/ReportnumberCNS-1054246
Project-/ReportnumberFP7/2007-2013
Project-/ReportnumberPIOF-GA-2012-328378
ISSN1572-8102
URNurn:nbn:at:at-ubl:3-1252 Persistent Identifier (URN)
DOI10.1007/s10703-016-0241-z 
Restriction-Information
 The work is publicly available
Files
ModelPlex [1.79 mb]
Links
Reference
Classification
Abstract (English)

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 with respect to the model. Otherwise, all bets are off. This article 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. ModelPlex ensures in a provably correct way 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. 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, assuming the system dynamics deviation is bounded. This article, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic by a correct-by-construction approach, leading to verifiably correct runtime model validation. Overall, ModelPlex generates provably correct monitor conditions that, if checked to hold at runtime, are provably guaranteed to imply that the offline safety verification results about the CPS model apply to the present run of the actual CPS implementation.

Stats
The PDF-Document has been downloaded 1 times.
License
CC-BY-License (4.0)Creative Commons Attribution 4.0 International License