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
06.11.2024
451502 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
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
|