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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal Verification of Clock Synchronization Algorithms for Aerospace Systems


    Contributors:


    Publication date :

    2024-11-06


    Size :

    451502 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Formal Verification of Safety-Critical Aerospace Systems

    Paul, Saswata / Cruz, Elkin / Dutta, Airin et al. | IEEE | 2023


    An Overview of Clock Synchronization Algorithms and their Uses in Aerospace and Automotive Systems

    de Oliveira Junior, Eloy Martins / de Oliveira e Souza, Marcelo Lopes | SAE Technical Papers | 2013


    Continuous Formal Verification for Aerospace Applications

    McColl, Morgan / McColl, Callum / Pereira, Aaron et al. | IEEE | 2024


    Formal Development of a Clock Synchronization Circuit

    Miner, P. / United States; National Aeronautics and Space Administration | British Library Conference Proceedings | 1995