Saved in:
Bibliographic Details
Main Authors: AP, Arif Ali, Babu, Jasine, John, Deepa Sara
Format: Preprint
Published: 2025
Subjects:
Online Access:https://arxiv.org/abs/2509.22236
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866915516532129792
author AP, Arif Ali
Babu, Jasine
John, Deepa Sara
author_facet AP, Arif Ali
Babu, Jasine
John, Deepa Sara
contents 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 $N$-modular redundant measurement system used for control applications in avionics systems. The work follows a correct-by-construction approach, using the Rocq theorem prover.
format Preprint
id arxiv_https___arxiv_org_abs_2509_22236
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle A Correct by Construction Fault Tolerant Voter for Input Selection of a Control System
AP, Arif Ali
Babu, Jasine
John, Deepa Sara
Logic in Computer Science
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 $N$-modular redundant measurement system used for control applications in avionics systems. The work follows a correct-by-construction approach, using the Rocq theorem prover.
title A Correct by Construction Fault Tolerant Voter for Input Selection of a Control System
topic Logic in Computer Science
url https://arxiv.org/abs/2509.22236