Combining Formal and Probabilistic Modeling in Resilient Systems Design

Resilience is a system property that enables a system (or system-of-systems) to continue to provide useful service in the face of disruptions. Resilience is especially important for systems that have to operate for extended periods in uncertain, disruptive environments. Resilience approaches today tend to be ad hoc and do not scale. Importantly, it is difficult to assess their long-term impact. This paper presents a flexible contract (FC) approach that employs a combination of formal methods for verification and testing and flexible assertions coupled with probabilistic modeling to handle mission uncertainty. A FC is a hybrid modeling construct that facilitates system verification and testing while offering the requisite flexibility to cope with non-determinism. This paper illustrates the use of FCs for multi-UAV swarm operations in, partially observable, dynamic environments. The approach is sufficiently general for use in other domains such as self-driving vehicles.