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 条

[21] Towards automatic generation of formal specifications for CML consistency verification
Sharbaf, Mohammadreza
Zamani, Bahman
Ladani, Behrouz Tork
2015 2ND INTERNATIONAL CONFERENCE ON KNOWLEDGE-BASED ENGINEERING AND INNOVATION (KBEI), 2015, : 860 - 865
[22] Formal consistency verification of deliberative agents with respect to communication protocols
Ramírez, J
de Antonio, A
FORMAL APPROACHES TO AGENT-BASED SYSTEMS, 2005, 3228 : 222 - 237
[23] Improving the consistency checking process by reusing formal verification knowledge
Redondo, RPD
Arias, JJP
Vilas, AF
Duque, JG
Solla, AG
PERSPECTIVES OF SYSTEM INFORMATICS, 2003, 2890 : 366 - 380
[24] Formal Synthesis of Stabilizing Controllers for Switched Systems
Prabhakar, Pavithra
Garcia Soto, Miriam
PROCEEDINGS OF THE 20TH INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (PART OF CPS WEEK) (HSCC' 17), 2017, : 111 - 120
[25] A Framework for Simulation and Formal Verification of Redundant Flight Control Systems with Components Subject to Partially Synchronous Timing Effects
Marvakov, Valentin A.
Holzapfel, Florian
2021 IEEE/AIAA 40TH DIGITAL AVIONICS SYSTEMS CONFERENCE (DASC), 2021,
[26] Toward Automated Attack Discovery in SDN Controllers Through Formal Verification
Yuan, Bin
Zhang, Chi
Ren, Jiajun
Chen, Qunjinming
Xu, Biang
Zhang, Qiankun
Li, Zhen
Zou, Deqing
Zhang, Fan
Jin, Hai
IEEE TRANSACTIONS ON NETWORK AND SERVICE MANAGEMENT, 2024, 21 (03): : 3636 - 3655
[27] Formal Verification of Neural Network Controllers for Collision-Free Flight
Genin, Daniel
Papusha, Ivan
Brule, Joshua
Young, Tyler
Mullins, Galen
Kouskoulas, Yanni
Wu, Rosa
Schmidt, Aurora
SOFTWARE VERIFICATION, 2022, 13124 : 147 - 164
[28] Formal Hardware/Software Co-Verification of Embedded Power Controllers
Dasgupta, Pallab
Srivas, Mandayam K.
Mukherjee, Rajdeep
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2014, 33 (12) : 2025 - 2029
[29] Modeling techniques for formal verification of BIST controllers and their integration into SOC designs
Roy, Subir K.
Parekhji, Rubin A.
20TH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS: TECHNOLOGY CHALLENGES IN THE NANOELECTRONICS ERA, 2007, : 364 - +
[30] Formal verification of privacy for RFID systems
Bruso, Mayla
Chatzikokolakis, Konstantinos
den Hartog, Jerry
2010 23RD IEEE COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2010, : 75 - 88

← 1 2 3 4 5 →