Papers › Modeling and Verifying Cyber-Physical Systems with Hybrid Active Objects
Modeling and Verifying Cyber-Physical Systems with Hybrid Active Objects
Formal modeling of cyber-physical systems (CPS) is hard, because they pose the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal specification and verification languages for CPS are designed on top of their underlying proof search technology. They lack high-level structuring elements. In addition, they are not efficiently executable. This makes formal CPS models hard to understand and to validate, hence impairs their usability. Instead, we suggest to model CPS in an Active Objects (AO) language designed for concise, intuitive modeling of concurrent systems. To this end, we extend the AO language ABS and its runtime environment with Hybrid Active Objects (HAO). CPS models and requirements formalized in HAO must follow certain communication patterns that permit automatic translation into differential dynamic logic, a sequential hybrid program logic. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the practicality of our approach with case studies.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Tasks
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Methods
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections