Document Open Access Logo

A Correct by Construction Fault Tolerant Voter for Input Selection of a Control System

Authors Arif Ali AP , Jasine Babu , Deepa Sara John

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2025.6.pdf
  • Filesize: 0.86 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Automated reasoning
Keywords
  • Fault Tolerant System Design
  • Formal Verification
  • Correct by Construction
  • Input Selection
  • Interactive Theorem Proving

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSTTCS.2025.6

Author Details

Arif Ali AP
  • Department of Computer Science and Engineering, Indian Institute of Technology Palakkad, India
Jasine Babu
  • Department of Computer Science and Engineering, Indian Institute of Technology Palakkad, India
Deepa Sara John
  • ISRO Inertial Systems Unit, Indian Space Research Organization, Thiruvananthapuram, India

Funding

A part of this work is funded by Indian Space Research Organisation (ISRO) RESPOND project RES-IISU-2022-013 titled `Formal Analysis and Verification of Redundancy Management Logic for Navigation Processor used in Man-rated Launch Vehicle'.

Acknowledgements

The authors acknowledge Saarang S and Mis Ab VP, former undergraduate students of IIT Palakkad, for their involvement in preliminary experiments with the Coq implementation of the voter, and Sandra S, visiting student at IIT Palakkad, for testing support. The authors also thank Murali Krishnan, Professor, National Institute of Technology Calicut, for his useful feedback on the initial draft.

Supplementary Materials

References

  1. Arif AP, Jasine Babu, and Deepa Sara John. A Correct by Construction Fault Tolerant Voter for Input Selection of a Control System, 2025. URL: https://arxiv.org/abs/2509.22236.
  2. A. Aviziens. Fault-tolerant systems. IEEE Transactions on Computers, C-25(12):1304-1312, 1976. URL: https://doi.org/10.1109/TC.1976.1674598.
  3. Ricky Butler and Sally Johnson. Formal Methods For Life-Critical Software, pages 319-329. Aerospace Research Central, October 1993. URL: https://doi.org/10.2514/6.1993-4516.
  4. Adam Chlipala. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, 2013. Google Scholar
  5. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8.
  6. Samar Dajani-Brown, Darren Cofer, Gary Hartmann, and Steve Pratt. Formal modeling and analysis of an avionics triplex sensor voter. In Model Checking Software, pages 34-48, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-44829-2_3.
  7. Daniel Davies and John F. Wakerly. Synchronization and matching in redundant systems. IEEE Transactions on Computers, C-27:531-539, 1978. URL: https://doi.org/10.1109/TC.1978.1675144.
  8. J Gloria Davis. An analysis of redundancy management algorithms for asynchronous fault tolerant control systems. Technical report, Ames Research Center, California, NASA, 1987. Google Scholar
  9. Analog Devices. ADIS1675 Datasheet. Accessed: 2025-07-10. URL: https://www.analog.com/en/products/adis16575.html.
  10. Ben L DiVito, Ricky W Butler, and James L Caldwell. Formal design and verification of a reliable computing platform for real-time control. Phase 1: Results. Technical report, NASA Langley Research Center, 1990. Google Scholar
  11. Jack Goldberg, Milton W. Green, William H. Kautz Karl N. Levitt, P. Michael Melliar-Smith, Richard L. Schwartz, and Charles B. Weinstoc. Development and analysis of the software implemented fault-tolerance (sift) computer. Technical report, SRI International, Menlo Park, California, 1984. Google Scholar
  12. E.F. Hitt and D. Mulcare. Fault-tolerant avionics. In C.R. Spitzer and Spitzer, editors, Digital Avionics Handbook (1st ed.), chapter 28, pages 1-28. CRC Press, 2006. URL: https://doi.org/10.1201/9781420036879.
  13. Honeywell. GG1320 User manual. Accessed: 2025-07-10. URL: https://aerospace.honeywell.com/content/dam/aerobt/en/documents/learn/products/sensors/user-manuals/GG1320-usermanual.pdf.
  14. Benjamin F. Jones and Lee Pike. Modular model-checking of a byzantine fault-tolerant protocol. In NASA Formal Methods, pages 163-177, Cham, 2017. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-57288-8_12.
  15. M. A. Kassab, H. S. Taha, S. A. Shedied, and A. Maher. A novel voting algorithm for redundant aircraft sensors. In Proceeding of the 11th World Congress on Intelligent Control and Automation, pages 3741-3746, 2014. URL: https://doi.org/10.1109/WCICA.2014.7053339.
  16. J.C. Knight. Safety critical systems: challenges and directions. In Proceedings of the 24th International Conference on Software Engineering. ICSE 2002, pages 547-550, 2002. Google Scholar
  17. Ranjani Krishnan. Simulation and application of voting algorithms for safety critical systems. In 2020 4th International Conference on Electronics, Communication and Aerospace Technology (ICECA), pages 1145-1150, 2020. URL: https://doi.org/10.1109/ICECA49313.2020.9297585.
  18. Ranjani Krishnan, Ashutosh Gupta, Nitin Chandrachoodan, and V R Lalithambika. Formal verification of clock synchronization algorithms for aerospace systems. In 2024 8th International Conference on Electronics, Communication and Aerospace Technology (ICECA), pages 1603-1608, 2024. URL: https://doi.org/10.1109/ICECA63461.2024.10800832.
  19. Ranjani Krishnan, Ashutosh Gupta, Nitin Chandrachoodan, and VR Lalithambika. Formal verification of voting algorithms for safety critical systems using two approaches. In 2024 IEEE Space, Aerospace and Defence Conference (SPACE), pages 211-215. IEEE, 2024. Google Scholar
  20. Leslie Lamport, Robert Shostak, and Marshall Pease. The Byzantine generals problem. ACM Trans. Program. Lang. Syst., 4(3):382-401, July 1982. URL: https://doi.org/10.1145/357172.357176.
  21. Patrick Lincoln and John Rushby. The formal verification of an algorithm for interactive consistency under a hybrid fault model. In Computer Aided Verification, pages 292-304, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-56922-7_24.
  22. Steven P. Miller, Alan C. Tribble, and Mats P. E. Heimdahl. Proving the shalls. In Keijiro Araki, Stefania Gnesi, and Dino Mandrioli, editors, FME 2003: Formal Methods, pages 75-93, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. Google Scholar
  23. Paul S Miner. Verification of fault-tolerant clock synchronization systems. Technical report, NASA Langley Research Center, 1993. Google Scholar
  24. M. Nicolaidis. Soft Errors In Modern Electronic Systems. Springer New York, NY, January 2011. URL: https://doi.org/10.1007/978-1-4419-6993-4.
  25. S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107-125, 1995. URL: https://doi.org/10.1109/32.345827.
  26. L. Pike. A note on inconsistent axioms in rushby’s "systematic formal verification for fault-tolerant time-triggered algorithms". IEEE Transactions on Software Engineering, 32(5):347-348, 2006. URL: https://doi.org/10.1109/TSE.2006.41.
  27. D. Powell. Failure mode assumptions and assumption coverage. In [1992] Digest of Papers. FTCS-22: The Twenty-Second International Symposium on Fault-Tolerant Computing, pages 386-395, 1992. URL: https://doi.org/10.1109/FTCS.1992.243562.
  28. Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Esteves-Verissimo. Velisarios: Byzantine fault-tolerant protocols powered by Coq. In Programming Languages and Systems, Cham, 2018. Springer International Publishing. Google Scholar
  29. J. Rushby. Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Transactions on Software Engineering, 25(5):651-660, 1999. URL: https://doi.org/10.1109/32.815324.
  30. J.M. Rushby and F. von Henke. Formal verification of algorithms for critical systems. IEEE Transactions on Software Engineering, 19(1):13-23, 1993. URL: https://doi.org/10.1109/32.210304.
  31. John Rushby. A formally verified algorithm for clock synchronization under a hybrid fault model. In Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, PODC '94, pages 304-313, New York, NY, USA, 1994. Association for Computing Machinery. URL: https://doi.org/10.1145/197917.198115.
  32. John Rushby. An overview of formal verification for the time-triggered architecture. In Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 83-105, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-45739-9_7.
  33. John Rushby and Frieder VonHenke. Formal verification of a fault tolerant clock synchronization algorithm. Technical report, NASA Langley Research Center, 1989. Google Scholar
  34. Indranil Saha, Suman Roy, and S. Ramesh. Formal verification of fault-tolerant startup algorithms for time-triggered architectures: A survey. Proceedings of the IEEE, 104:1-19, March 2016. URL: https://doi.org/10.1109/JPROC.2016.2519247.
  35. Rocq Core Team. Program extraction. Accessed: 2025-07-08. URL: https://rocq-prover.org/doc/master/refman/addendum/extraction.html.
  36. Rocq Core Team. Rocq prover. Accessed: 2025-07-08. URL: https://rocq-prover.org/.
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