Copilot: Monitor Synthesis for Software Health Management
In this NASA-funded project, Galois and NASA built software to detect failures in commercial avionics systems.
Avionics systems are inherently distributed, real-time systems that must take into account system-level properties and the environment, not just the implementation of software subsystems.
Avionics software is large and complex, some systems containing millions of lines of code. With today’s technology, it is infeasible to formally verify entire systems for correctness. Therefore, we investigated the use of runtime monitoring to detect software and system failures.
In this project, we built a new language, Copilot, for specifying distributed monitors and for synthesizing them. Copilot is a domain-specific, embedded stream language for generating hard real-time C code. It is specifically developed to write embedded software monitors for more complex embedded systems, but it can be used to develop a variety of functional-style embedded code.
As part of this project, we performed flight tests on a NASA UAV to detect pitot tubes sensor failures.