Keynote talk I: Building a high-assurance unpiloted air vehicle
Lee Pike · Formal Methods · 2013
Summary form only given. A drone autopilot is a complex software artifact that includes operating systems, networking, and sensor systems. With support from DARPA, Galois is addressing the challenge of building an open-source high-assurance autopilot that is resistant to security attacks and software faults. We are tackling the problem by borrowing from a suite of formal-methods-inspired technologies such as strongly-typed domain-specific languages for embedded control systems, software model-checking, and runtime-verification. Just over one year in, we have designed two new languages and compilers and have a provisional autopilot developed. I will describe how we have achieved low-cost high-assurance software, and I will elaborate on the challenges ahead and the open problems we do not yet know how to address. For more information related to the autopilot, see smaccmpilot.org.