In man-rated missions of launch vehicles, quadruple redundancy is generally provided for the different subsystems. In this work, the extension of the master-slave algorithm and a convergence averaging scheme for clock synchronization were studied and validated through formal methods. The results proved that the specified properties are satisfied in both the schemes. The averaging scheme has the advantage of simplicity and consequently executes with lesser resources. The main contribution is the definition of a methodical process for modelling and verification of embedded software in the Ada language using two varied approaches. The application of the techniques to a real case study proved its efficacy in establishing the correctness of the software in critical systems.
Formal Verification of Clock Synchronization Algorithms for Aerospace Systems
2024-11-06
451502 byte
Conference paper
Electronic Resource
English
Formal Verification of Safety-Critical Aerospace Systems
IEEE | 2023
|An Overview of Clock Synchronization Algorithms and their Uses in Aerospace and Automotive Systems
SAE Technical Papers | 2013
|Formal Development of a Clock Synchronization Circuit
British Library Conference Proceedings | 1995
|Traveling clock verification of VLBI synchronization
NTRS | 1979
|