Component-Driven Roller Coaster Verification

CoasterX is a the first toolchain for designing and verifying 2-dimensional roller coaster track designs. In addition providing results for real coasters, CoasterX serves as a case study in what we dub component-driven automation, the technique of generating and verifying formal models of a design completely automatically by exploiting the structure of a component model built in a design tool. This makes the verification results accessible even to users without formal methods knowledge.

The CoasterX frontend allows component-based click-and-point design of roller coasters by placing consecutive track sections. The backend, implemented in Scala on top of the KeYmaera X theorem prover, then extract and verifies a specification in differential dynamic logic exhibiting bounds on velocity and acceleration of the train. From these bounds, we can information about safety issues including rollbacks, stuck coasters, derailment, and medical risks imposed by accelerations themselves.

CoasterX has been applied to several real coasters, including the Steel Phantom and its gentler successor Phantom's Revenge at Kennywood in West Mifflin, PA. We show that CoasterX's acceleration bounds can distinguish the rougher Steel Phantom from the Phantom's Revenge by a wide margin.