Abstract :
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.
Keywords :
aerospace computing; autonomous aerial vehicles; formal verification; mobile robots; security of data; telerobotics; Galois; drone autopilot; embedded control systems; formal methods; networking systems; operating systems; runtime verification; security attacks; sensor systems; software artifact; software faults; software model checking; unpiloted air vehicle; Abstracts; Buildings; Control systems; NASA; Operating systems; Vehicles;
