A Correct by Construction Fault Tolerant Voter for Input Selection of a Control System
Logic in Computer Science
2025-09-29 v1
Abstract
Safety-critical systems use redundant input units to improve their reliability and fault tolerance. A voting logic is then used to select a reliable input from the redundant sources. A fault detection and isolation rules help in selecting input units that can participate in voting. This work deals with the formal requirement formulation, design, verification and synthesis of a generic voting unit for an -modular redundant measurement system used for control applications in avionics systems. The work follows a correct-by-construction approach, using the Rocq theorem prover.
Keywords
Cite
@article{arxiv.2509.22236,
title = {A Correct by Construction Fault Tolerant Voter for Input Selection of a Control System},
author = {Arif Ali AP and Jasine Babu and Deepa Sara John},
journal= {arXiv preprint arXiv:2509.22236},
year = {2025}
}