Formal methods are seen as a cheaper and more exhaustive solution to the current expensive testing process used in the aviation industry. However, aviation systems are getting more and more complex. So, formal methods have no hope to address these systems unless some compositional argument is being made. In this talk, I will present the results of the effort led by NASA to demonstrate the use of formal methods and compositional verification for the V&V of safety requirements of a flight critical system. The talk will show how the formal arguments made at the component level are being composed into a system-level argument. The study is done on Simulink models for a quad-redundant flight control system for a transport class airplane.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Compositional verification using formal analysis for a flight critical system


    Contributors:


    Publication date :

    2014-10-01


    Size :

    30477 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Formal Verification of Flight Critical Software

    Miller, Steven / Anderson, Elise / Wagner, Lucas et al. | AIAA | 2005



    Formal Verification of Quadcopter Flight Envelop Using Theorem Prover

    Jasim, Omar A. / Veres, Sandor M. | IEEE | 2018


    Verification of Flight Critical Systems

    Goossen, Emray | SAE Technical Papers | 1990


    An approach to formal verification of free-flight separation

    Eder, S. / Smith, G. | Tema Archive | 2010