Fault Centered Robustness in TLA+

Robustness

TLA+

Distributed Protocols

The guarantees provided by formal verification are only as good as the assumptions that are made about the environment. Therefore, in prior work, we have proposed robustness analysis to help system designers how robust their guarantees are to environmental deviations. In this project, we lift the notion of robustness to symbolic transition systems in fault-centered robustness, in which we calculate safe environmental envelopes based on a user-given set of symbolic faults.