TRS Project

Team:

• Cordell Green (PI)
• Stephen Fitzpatrick (Co-PI)
• Alessandro Coglio
• Christoph Kreitz
• Eric Smith
• Stephen Westfold

This project is funded by AFRL. Our goal is to use formal program synthesis technology to generate software that, besides being trusted (by virtue of the formal proofs), is also resilient. Here, resilience refers to the ability of the software to adapt to unforeseen changes in the assumptions under which it was designed to operate, e.g. changes in environmental assumptions.

Our approach is the following. We start with an implementation of the software that has been formally derived from a specification, using the APT toolkit. Specification and derivation incorporate the assumptions under which the software was created. When these assumptions change, we represent their changes formally as updates to the specification and derivation. Re-processing the updated specification derivation generates an updated implementation that works as intended under the new assumptions. This re-synthesis process is simpler than synthesizing the new version from scratch.

We are looking at two sample applications. One is a resilient drone fleet planner. Another one is the resilient Flex prover/solver.