Search Results

Documents authored by Ali AP, Arif

Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.6
A Correct by Construction Fault Tolerant Voter for Input Selection of a Control System

Authors: Arif Ali AP, Jasine Babu, and Deepa Sara John

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

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 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.
Cite as

Arif Ali AP, Jasine Babu, and Deepa Sara John. A Correct by Construction Fault Tolerant Voter for Input Selection of a Control System. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aliap_et_al:LIPIcs.FSTTCS.2025.6,
  author =	{Ali AP, Arif and Babu, Jasine and John, Deepa Sara},
  title =	{{A Correct by Construction Fault Tolerant Voter for Input Selection of a Control System}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{6:1--6:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.6},
  URN =		{urn:nbn:de:0030-drops-250886},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.6},
  annote =	{Keywords: Fault Tolerant System Design, Formal Verification, Correct by Construction, Input Selection, Interactive Theorem Proving}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact