New air traffic management concepts distribute the duty of traffic separation among system participants. As a consequence, these concepts have a greater dependency and rely heavily on on-board software and hardware systems. One example of a new on-board capability in a distributed air traffic management system is air traffic conflict detection and resolution (CD&R). Traditional methods for safety assessment such as human-in-the-loop simulations, testing, and flight experiments may not be sufficient for this highly distributed system as the set of possible scenarios is too large to have a reasonable coverage. This paper proposes a new method for the safety assessment of avionics systems that makes use of formal methods to drive the development of critical systems. As a case study of this approach, the mechanical veri.cation of an algorithm for air traffic conflict resolution and recovery called RR3D is presented. The RR3D algorithm uses a geometric optimization technique to provide a choice of resolution and recovery maneuvers. If the aircraft adheres to these maneuvers, they will bring the aircraft out of conflict and the aircraft will follow a conflict-free path to its original destination. Veri.cation of RR3D is carried out using the Prototype Verification System (PVS).


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

    Formal Verification of a Conflict Resolution and Recovery Algorithm


    Beteiligte:
    Maddalon, Jeffrey (Autor:in) / Butler, Ricky (Autor:in) / Geser, Alfons (Autor:in) / Munoz, Cesar (Autor:in)

    Erscheinungsdatum :

    01.04.2004


    Medientyp :

    Report


    Format :

    Keine Angabe


    Sprache :

    Englisch




    Formal Verification of a Conflict Resolution and Recovery Algorithm

    J. Maddalon / R. Butler / A. Geser et al. | NTIS | 2004


    FORMAL VERIFICATION OF SAFETY BUFFERS FOR STATE-BASED CONFLICT DETECTION AND RESOLUTION

    Herencia-Zapana, H. / Jeannin, J.-B. / Munoz, C. et al. | British Library Conference Proceedings | 2010


    On the Formal Verification of Conflict Detection Algorithms

    Munoz, Cesar / Butler, Ricky W. / Carreno, Victor A. et al. | NTRS | 2001


    Formal Verification of Air Traffic Conflict Prevention Bands Algorithms

    Narkawicz, Anthony J. / Munoz, Cesar A. / Dowek, Gilles | NTRS | 2010


    Safety verification of conflict resolution manoeuvres

    Tomlin, C. / Mitchell, I. / Ghosh, R. | IEEE | 2001