As part of DARPA's High Assurance Cyber Military Systems (HACMS), Galois is building critical flight control software using new software methods for embedded systems programming. Recently, Signal Online reported an overview of the HACMS program. We've been working on the HACMS program for about a year and we'd like to share more details about open source work we've done so far.
The flagship application for the technologies we've developed under the HACMS program is called SMACCMPilot: a new flight controller for small quadcopter unmanned aerial vehicles (UAVs). SMACCMPilot is written in the Ivory language, a new domain-specific language for safe systems programming. We've built an ecosystem of libraries on top of the Ivory language, including a concurrency framework and drivers for microcontroller hardware. Ivory has a simple interface to external C code, which allows SMACCMPilot to re-use software components from the ArduCopter open source project. We've also implemented communications protocol stacks and control primitives in Ivory. SMACCMPilot is currently alpha-quality software as we actively develop the flight control software itself and evolve the new technologies we've used to build it. We'll be continuing work on the SMACCMPilot project for the next few years.
All of the software behind SMACCMPilot is open source and available on Galois's github, and documented on the project web site. We welcome collaboration with programming languages, formal methods, and flight control researchers!