具有冗余控制器系统的一致性形式化验证
软件工程
2024-03-29 v1
摘要
在分布式控制系统领域可能出现的一个潜在问题是，冗余方案中存在多个主控制器，这可能导致不一致性。一种名为 NRP FD 的算法被提出以通过优先保证一致性而非可用性来解决此问题。在本文中，我们展示了如何通过使用建模和形式化验证，发现 NRP FD 中可能同时存在两个主控制器的问题。随后，我们提供了一种缓解该已识别问题的解决方案，从而增强了此类系统的鲁棒性和可靠性。
引用
@article{arxiv.2403.18917,
title = {Formal Verification of Consistency for Systems with Redundant Controllers},
author = {Bjarne Johansson and Bahman Pourvatan and Zahra Moezkarimi and Alessandro Papadopoulos and Marjan Sirjani},
journal= {arXiv preprint arXiv:2403.18917},
year = {2024}
}
备注
In Proceedings MARS 2024, arXiv:2403.17862