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 |