Reproduce “Formal Verification of Consistency for Systems with Redundant Controllers” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Bjarne Johansson, Bahman Pourvatan, Zahra Moezkarimi, Alessandro Papadopoulos, Marjan Sirjani
Researchers formally verified the Network Reference Point Failure Detection (NRP FD) algorithm for redundant industrial controllers, uncovering specific scenarios where the original design could lead to conflicting primary controllers. An enhanced version, Leasing NRP FD, was then developed and formally proven to maintain single-primary consistency, even under complex failure conditions.
Key insights
- Formal verification revealed critical vulnerabilities in the original NRP FD, showing that simultaneous primary network switch failures or transient heartbeat disruptions could lead to an inconsistent dual primary state.
- The temporal separation and independent disruption of heartbeat signals versus NRP communication in the original design introduced a root cause for inconsistency under specific, hard-to-test failure modes.
- Implementing a timestamp-based leasing mechanism through the Network Reference Point effectively ensures that only one primary can hold a valid 'lease' at any given time, thereby resolving dual primary issues and upholding consistency.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.