ModelPlex: verified runtime validation of verified cyber-physical system models

DOI10.1007/s10703-016-0241-zzbMath1380.68282OpenAlexW2127240436WikidataQ59477568 ScholiaQ59477568MaRDI QIDQ681465

Stefan Mitsch, André Platzer

Publication date: 12 February 2018

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-016-0241-z

zbMATH Keywords

hybrid systemsruntime verificationcyber-physical systemsdifferential dynamic logicstatic verification

Mathematics Subject Classification ID

Control/observation systems involving computers (process control, etc.) (93C83) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Related Items (10)

Constructive Game Logic ⋮ Pegasus: sound continuous invariant generation ⋮ Offline and online monitoring of scattered uncertain logs using uncertain linear dynamical systems ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ On proving that an unsafe controller is not proven safe ⋮ Linearization, model reduction and reachability in nonlinear ODEs ⋮ Verifiably safe exploration for end-to-end reinforcement learning ⋮ ModelPlex: verified runtime validation of verified cyber-physical system models ⋮ A formally verified, optimized monitor for metric first-order dynamic logic ⋮ Constructive hybrid games

Uses Software

• QEPCAD
• KeYmaera
• dReal
• SpaceEx
• Java-MOP
• ModelPlex
• AMT
• KeYmaera X
• LOLA

Cites Work

• Unnamed Item
• ModelPlex: verified runtime validation of verified cyber-physical system models
• Differential dynamic logic for hybrid systems
• Real quantifier elimination is doubly exponential
• Partial cylindrical algebraic decomposition for quantifier elimination
• Factorization of a hierarchy of the lattice soliton equations from a binary Bargmann symmetry constraint
• A brief account of runtime verification
• SMT-based scenario verification for hybrid systems
• Logics of Dynamical Systems
• The Complete Proof Theory of Hybrid Systems
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• A Uniform Substitution Calculus for Differential Dynamic Logic
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• The Image Computation Problem in Hybrid Systems Model Checking
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Logical Analysis of Hybrid Systems
• Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems

This page was built for publication: ModelPlex: verified runtime validation of verified cyber-physical system models