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
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.