Formal Verification of Clock Synchronization Algorithms for Aerospace Systems

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.