Formal Methods in Resilient Systems Design: Application to Multi-UAV System-of-Systems Control

Abstract

Resilience approaches today rely on ad hoc methods that offer piecemeal solutions. Models used by these methods are difficult to verify and do not scale. Furthermore, it is difficult to assess their long-term impact. This chapter presents a resilient systems design approach based on formal methods that is intended to overcome these limitations. The approach combines deterministic and probabilistic modeling to create a new modeling construct that lends itself to designing scalable, resilient systems and system-of-systems (SoS). The formalism facilitates model verification and possesses requisite flexibility to handle nondeterminism. The target application domain is multi-UAV swarm control in uncertain, potentially hazardous, dynamic environments. However, the approach is sufficiently general for a variety of SoS including autonomous vehicle SoS networks.