2026-08-07T18:21:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19296 2025-10-09T13:18:07Z ddc:004 open_access

A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems Kamburjan, Eduard Mitsch, Stefan Hähnle, Reiner Active Objects Differential Dynamic Logic Hybrid Systems Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Eduard Kamburjan and Stefan Mitsch and Reiner Hähnle 2022 Is Part Of LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2 Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LITES.8.2.4 urn:nbn:de:0030-drops-192965 https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.4 eng https://creativecommons.org/licenses/by/4.0/legalcode