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.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal Verification of Clock Synchronization Algorithms for Aerospace Systems


    Beteiligte:


    Erscheinungsdatum :

    06.11.2024


    Format / Umfang :

    451502 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    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