Resilience of Systems under Maximum Component Deviations.
Author
Abstract

Software systems are composed of interacting processes that send data to satisfy system-level requirements. When these processes become unavailable due to deviations in the system – software bugs, hardware failures, or security attacks – these systems should be resilient and continue delivering safety-critical services. Identifying the processes required to satisfy these requirements is not a trivial task as there may exists multiple, alternate dataflow paths to satisfy the requirements. In this work, we propose a formal modeling and analysis technique to compute the sets of minimal processes required for dataflow satisfaction. The computation of these sets is reduced to a maximum satisfiability problem via translation to AlloyMax, a formal modeling language that performs bounded model-checking. We then present a method to formally define the resilience requirements for a system by constraining the minimal dataflow required under maximum system deviation. The efficacy of this work is then evaluated with four case studies motivated from real-world systems with promising results.

Year of Publication
2025
Conference Name
23rd International Conference on Software Engineering and Formal Methods
Conference Location
Toledo, Spain
Google Scholar | BibTeX