SCS Undergraduate Thesis Topics
|Annika Peterson||Andre Platzer||Formal Verification of a Controlled Flight Between Two Robots: A Case Study|
Robots moving within controlled flight paths are complex systems that require formal verification of collision avoidance. A flight path dependent upon a coded program requires confidence of its ability to avoid crashing, which we show with a formal proof. Inspired by the controlled flight of two robots within the Disney-Pixar film WALLb"E, we have designed a controller for a robot flying within a complex controlled flight path, a helix with another robot. We have formally proven collision avoidance within the proof rules of differential dynamic logic, a logic for hybrid systems consisting of discrete controlled steps and continuous physics, using a deductive verification tool, KeYmaera, when this flight path is viewed in two dimensions as well as three dimensions. We formally prove safety as well as an additional property that the two robots are within some delta of each other. This case study also applies to aircraft collision avoidance and unmanned aerial vehicles where unsafe operation is potentially fatal and similar 3D motion is relevant.