Formal Methods in Resilient Systems Design using a Flexible Contract Approach
Technical Report,09 Aug 2016,21 Dec 2018
SYSTEMS ENGINEERING RESEARCH CENTER HOBOKEN NJ HOBOKEN United States
Pagination or Media Count:
Resilience is a much-needed characteristic in systems that are expected to operate in uncertain, disruptive environments for extended periods. Resilience approaches today employ ad hoc methods and piece-meal solutions that are difficult to verify and test, and do not scale. Furthermore, it is difficult to assess the long-term impact of such ad hoc resilience solutions. This research presents a flexible contract-based approach that employs a combination of formal methods for verification and testing and flexible assertions and probabilistic modeling to handle uncertainty during mission execution. A flexible contract FC is a hybrid modeling construct that facilitates system verification and testing while offering the requisite flexibility to cope with non-determinism. This research illustrates the use of FCs for multi-UAV swarm control in partially observable, dynamic environments. However, the approach is sufficiently general for use in other domains such as self-driving vehicle and adaptive powerenergy grids.
- Administration and Management