Developments in autonomous aircraft, such as electrical vertical take-off and landing vehicles and multicopter drones, raise safety-critical concerns in populated areas. This article presents the Analysis of Safety-Critical Systems Using Formal Methods-Based Runtime Evaluation (ASSURE) framework, which is a collection of techniques for aiding in the formal verification of safety-critical aerospace systems. ASSURE supports the rigorous verification of deterministic and nondeterministic properties of both distributed and centralized aerospace applications by using formal theorem proving tools. We present verifiable algorithms and software, formal reasoning models, formal proof libraries, and a data-driven runtime verification approach for aerospace systems toward a provably safe Internet of Planes infrastructure.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal Verification of Safety-Critical Aerospace Systems


    Contributors:


    Publication date :

    2023-05-01


    Size :

    6502298 byte




    Type of media :

    Article (Journal)


    Type of material :

    Electronic Resource


    Language :

    English



    Continuous Formal Verification for Aerospace Applications

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


    Formal Verification of Clock Synchronization Algorithms for Aerospace Systems

    Krishnan, Ranjani / Gupta, Ashutosh / Chandrachoodan, Nitin et al. | IEEE | 2024


    A Viable Approach to Formal Verification of Complex Aerospace Systems

    Vaz, Eduardo / Elliott, Christopher M. / Stanfill, Peter O. | AIAA | 2019


    Formal verification in the loop to enhance verification of safety-critical cyber-physical systems

    Cinzia Bernardeschi / Andrea Domenici / Sergio Saponara | BASE | 2019

    Free access

    Integrated Formal Verification and Validation of Safety Critical Software

    Ward, N. J. / North Atlantic Treaty Organization | British Library Conference Proceedings | 1993