Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B

DOI10.1007/978-3-319-91271-4_11MaRDI QIDQ5881449zbMATH OpenOpenAlexFDO

Authors Guillaume Dupont, Yamine Ait-Ameur, Marc Pantel, Neeraj Kumar Singh

Publication date 10 March 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-91271-4_11

zbMATH Keywords

hybrid systemsrefinementEvent-Bdifferential dynamic logichybrid programs

Mathematics Subject Classification ID

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) Logic in computer science (03B70)

Recommendations

• A hybrid dynamic logic for event/data-based systems
• scientific article; zbMATH DE number 1522990
• Towards a hybrid dynamic logic for hybrid dynamic systems
• Hybrid dynamic logic institutions for event/data-based systems
• The Complete Proof Theory of Hybrid Systems
• Differential Logic for Reasoning About Hybrid Systems

Cites work

• Differential dynamic logic for hybrid systems
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Modeling in Event B. System and software engineering.
• Practical theory extension in Event-B
• Trusting computations: a mechanized proof from partial differential equations to actual program

Cited in

(5)

• Constructive Formalization of Hybrid Logic with Eventualities
• A refinement-based formal development of cyber-physical railway signalling systems
• Reachability analysis and simulation for hybridised Event-B models
• Component based design of hybrid systems: a case study on concurrency and coupling
• scientific article; zbMATH DE number 2000404 (Why is no real title available?)

Describes a project that uses

Uses Software

• Rodin
• KeYmaera

This page was built for publication: Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5881449)