Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal Verification of Consistency for Systems with Redundant Controllers

Bjarne Johansson, Bahman Pourvatan, Zahra Moezkarimi, Alessandro Papadopoulos, Marjan Sirjani

TL;DR

This work confronts the risk of two primary controllers arising in redundant distributed control networks by formalizing and validating the Network Reference Point Failure Detection (NRP FD) algorithm with Timed Rebeca and Afra, focusing on the safety property $NoDualPrimary$. It demonstrates that certain failure scenarios can yield dual primaries and introduces Leasing NRP FD as an enhanced scheme that enforces a single primary even under transient disturbances. Through formal modeling, verification, and counterexample exploration, the authors identify corner cases and quantify state-space growth (e.g., 15891 states for Leasing NRP FD with 34053 transitions). The approach provides a rigorous path toward more robust, consistency-preserving redundancy in industrial DCN environments, with potential extensions to dynamic topologies and probabilistic analyses for availability trade-offs.

Abstract

A potential problem that may arise in the domain of distributed control systems is the existence of more than one primary controller in redundancy plans that may lead to inconsistency. An algorithm called NRP FD is proposed to solve this issue by prioritizing consistency over availability. In this paper, we demonstrate how by using modeling and formal verification, we discovered an issue in NRP FD where we may have two primary controllers at the same time. We then provide a solution to mitigate the identified issue, thereby enhancing the robustness and reliability of such systems.

Formal Verification of Consistency for Systems with Redundant Controllers

TL;DR

This work confronts the risk of two primary controllers arising in redundant distributed control networks by formalizing and validating the Network Reference Point Failure Detection (NRP FD) algorithm with Timed Rebeca and Afra, focusing on the safety property . It demonstrates that certain failure scenarios can yield dual primaries and introduces Leasing NRP FD as an enhanced scheme that enforces a single primary even under transient disturbances. Through formal modeling, verification, and counterexample exploration, the authors identify corner cases and quantify state-space growth (e.g., 15891 states for Leasing NRP FD with 34053 transitions). The approach provides a rigorous path toward more robust, consistency-preserving redundancy in industrial DCN environments, with potential extensions to dynamic topologies and probabilistic analyses for availability trade-offs.

Abstract

A potential problem that may arise in the domain of distributed control systems is the existence of more than one primary controller in redundancy plans that may lead to inconsistency. An algorithm called NRP FD is proposed to solve this issue by prioritizing consistency over availability. In this paper, we demonstrate how by using modeling and formal verification, we discovered an issue in NRP FD where we may have two primary controllers at the same time. We then provide a solution to mitigate the identified issue, thereby enhancing the robustness and reliability of such systems.
Paper Structure (14 sections, 11 figures, 1 table)

This paper contains 14 sections, 11 figures, 1 table.

Table of Contents

  1. Introduction
  2. Network Reference Point Failure Detection (NRP FD) Algorithm
  3. Modeling and Verification of NRP FD using Timed Rebeca
  4. The actor-based language, Timed Rebeca
  5. Modeling NRP-FD in Timed Rebeca
  6. Model checking of NRP FD using Afra
  7. Leasing NRP FD
  8. Why Timed Rebeca?
  9. Related work
  10. Conclusion and Future Work
  11. Rebeca Syntax
  12. Afra
  13. Timed Rebeca model of the Leasing NRP FD
  14. State Space

Figures (11)

  • Figure 1: A redundant DCN (controller) pair synchronized with dedicated, redundant redundancy link.
  • Figure 2: Redundant controllers connected over a redundant, disjoint network backbone.
  • Figure 3: (a) F1 and F2 exemplify network failures partitioning the redundant controller pair, preventing the heartbeat (and other communication) between DCN 1 and DCN 2. (b) Due to F1 and F2 caused partitioning, both DCN 1 and DCN 2 become primary and drive potentially inconsistent outputs.
  • Figure 4: The redundant network backbone with the NRP and NRP candidates highlighted.
  • Figure 5: (L1) An abstracted version of the Timed Rebeca model of NRP FD (Full version in Appendix \ref{['app::TimedRebecaNRPFD']}).
  • ...and 6 more figures