ModelPlex: verified runtime validation of verified cyber-physical system models
From MaRDI portal
Publication:681465
cyber-physical systemsdifferential dynamic logichybrid systemsruntime verificationstatic verification
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) Control/observation systems involving computers (process control, etc.) (93C83)
Recommendations
Cites work
- A brief account of runtime verification
- A uniform substitution calculus for differential dynamic logic
- Differential dynamic logic for hybrid systems
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- Direct formal verification of liveness properties in continuous and hybrid dynamical systems
- dReal: an SMT solver for nonlinear theories over the reals
- Factorization of a hierarchy of the lattice soliton equations from a binary Bargmann symmetry constraint
- scientific article; zbMATH DE number 1444358 (Why is no real title available?)
- KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Logical analysis of hybrid systems. Proving theorems for complex dynamics.
- Logics of dynamical systems
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Partial cylindrical algebraic decomposition for quantifier elimination
- Real quantifier elimination is doubly exponential
- SMT-based scenario verification for hybrid systems
- The Complete Proof Theory of Hybrid Systems
- The Image Computation Problem in Hybrid Systems Model Checking
Cited in
(19)- Bellerophon: tactical theorem proving for hybrid systems
- IPL: an integration property language for multi-model cyber-physical systems
- A formally verified, optimized monitor for metric first-order dynamic logic
- Constructive hybrid games
- Pegasus: sound continuous invariant generation
- scientific article; zbMATH DE number 6719346 (Why is no real title available?)
- Constructive game logic
- Bridging the gap between single- and multi-model predictive runtime verification
- 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
- Pegasus: a framework for sound continuous invariant generation
- Model predictive runtime verification for cyber-physical systems with real-time deadlines
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Refining constructive hybrid games
- \textsc{Soteria}: a formal digital-twin-enabled framework for safety-assurance of latency-aware cyber-physical systems
- Linearization, model reduction and reachability in nonlinear \textsc{ODEs}
- Measuring robustness in cyber-physical systems under sensor attacks
- Uniform substitution for differential refinement logic
Describes a project that uses
Uses Software
This page was built for publication: ModelPlex: verified runtime validation of verified cyber-physical system models
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q681465)
