During the summer of 2017 we participated in Air Force Research Laboratory's (AFRL) Summer of Innovation (SoI) program. The program leveraged AFRL's Unmanned Systems Autonomy Services (UxAS) as a basis to create a truly modular, open, and verifiable in-house UAV autonomy architecture. The program was modeled after the "Google Summer of Code" program. It was a 14-week "innovation workshop" with a team of experts from academia, government, and industry working together in a facility located in downtown Dayton, OH. The team of approximately 50 experts in formal methods and software design leveraged an open source version of UxAS and the AFRL AMASE simulation platform to develop formal evidence for the correctness of the platform. When it was discovered that the existing system did not meet certain requirements, the team augmented UxAS in order to prove that it functioned as intended.
In this project we used our AADL analysis tools (AGREE and Resolute) to reason about properties of the UxAS architecture. We also applied technologies developed under the HACMS project to re-architect UxAS and formally prove that it met certain safety guarantees.
Slides from talks at S5 2017 describing our contributions can be found here:
UxAS + seL4
A video of our demonstration of UxAS + seL4 can be found here: