From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink

Arthur Amorim, Paul Gazzillo, Max Taylor +1

Standard communication protocols for Unmanned Aerial Vehicles (UAVs), such as MAVLink, lack the capability to enforce the contextual validity of message sequences. Autopilots there…