CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation

摘要

Component-driven proof automation (CDPA) exploits component structure to automate deductive verification of large-scale hybrid systems with non-trivial continuous dynamics. We use CDPA to implement a case study CoasterX, which is a toolchain for designing and verifying safety of 2-dimensional roller coaster track designs. Specifically, we verify velocity and acceleration bounds. CoasterX starts with a graphical front-end for point-and-click design of tracks. The CoasterX back-end then automatically specifies and verifies the track in differential dynamic logic (d?) with a custom procedure built in the KeYmaera X theorem prover. We show that the CDPA approach scales, testing real coasters of up to 56 components.