Formal Verification of Consistency for Systems with Redundant Controllers

被引：0

作者：

Johansson, Bjarne ^{[1
,2
]}

Pourvatan, Bahman ^{[2
]}

Moezkarimi, Zahra ^{[2
]}

Papadopoulos, Alessandro ^{[2
]}

Sirjani, Marjan ^{[2
]}

机构：

[1] ABB AB, Vasteras, Sweden

[2] Malardalen Univ, Vasteras, Sweden

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2024年 / 399期

关键词：

REBECA;

D O I：

10.4204/EPTCS.399.8

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：169 / 191

页数：23

共 50 条

[1] Formal verification of sequence controllers
Park, T
Barton, PI
COMPUTERS & CHEMICAL ENGINEERING, 2000, 23 (11-12) : 1783 - 1793
[2] Formal Verification of Stochastic Systems with ReLU Neural Network Controllers
Sun, Shiqi
Zhang, Yan
Luo, Xusheng
Vlantis, Panagiotis
Pajic, Miroslav
Zavlanos, Michael M.
2022 IEEE INTERNATIONAL CONFERENCE ON ROBOTICS AND AUTOMATION, ICRA 2022, 2022, : 6800 - 6806
[3] Formal verification for analysis and design of reconfigurable controllers for manufacturing systems
Kalita, D
Khargonekar, PP
PROCEEDINGS OF THE 2000 AMERICAN CONTROL CONFERENCE, VOLS 1-6, 2000, : 3533 - 3539
[4] Formal Verification of Grid Frequency Controllers
Mohapatra, Anurag
Peric, Vedran S.
Hamacher, Thomas
2021 IEEE PES INNOVATIVE SMART GRID TECHNOLOGY EUROPE (ISGT EUROPE 2021), 2021, : 643 - 648
[5] Formal verification for analysis and design of logic controllers for reconfigurable machining systems
Kalita, D
Khargonekar, PP
IEEE TRANSACTIONS ON ROBOTICS AND AUTOMATION, 2002, 18 (04): : 463 - 474
[6] A Framework for Formal Verification of DRAM Controllers
Steiner, Lukas
Sudarshan, Chirag
Jung, Matthias
Stoffel, Dominik
Wehn, Norbert
PROCEEDINGS OF THE INTERNATIONAL SYMPOSIUM ON MEMORY SYSTEMS, MEMSYS 2022, 2022,
[7] Formal verification of delayed consistency protocols
Pong, F
Dubois, M
10TH INTERNATIONAL PARALLEL PROCESSING SYMPOSIUM - PROCEEDINGS OF IPPS '96, 1996, : 124 - 131
[8] A FORMAL MODEL FOR VERIFICATION OF DYNAMIC CONSISTENCY OF KBSS
LAITA, LM
RAMIREZ, B
DELEDESMA, L
RISCOS, A
COMPUTERS & MATHEMATICS WITH APPLICATIONS, 1995, 29 (05) : 81 - 96
[9] Formal verification of redundant media extension of Ethernet PowerLink
Limal, Steve
Potier, Stephane
Denis, Bruno
Lesage, Jean-Jacques
ETFA 2007: 12TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOLS 1-3, 2007, : 1045 - +
[10] Formal Modeling and Verification of Controllers for a Family of DRAM Caches
Sahoo, Debiprasanna
Sha, Swaraj
Satpathy, Manoranjan
Mutyam, Madhu
Ramesh, S.
Roop, Partha
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2018, 37 (11) : 2485 - 2496

← 1 2 3 4 5 →