Verification of aircraft control algorithm at the model level is a challenge. Formal methods play a critical role in mathematically analysing the functionality and completeness of the algorithm. The advantage of using formal method is that it helps in mathematical analysis of complex algorithms for the correctness and guarantees the properties of a particular model using formal verifiers. The project entails the development of a workflow which verifies the correctness of a safety critical embedded system. The workflow is proven by implementing the Mode Transition Logic (MTL) for Autopilot and Stall Warning System model, taken as a case study. The proposed workflow provides a seamless syntactic translation of Simulink Model(s) into probabilistic models with Markov properties, for PRISM Model Checker. This will help in re-assuring the integrity of the model, an integrated module of safety critical systems among various applications such as Aerospace, Automobile, Medical, and Industrial domain.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Validation of control algorithm using formal methods: Validation of mode transition logic of AFCS in SARAS aircraft


    Contributors:


    Publication date :

    2017-03-01


    Size :

    2423876 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    AFCS Integration Requirements

    Chmaruk, B. H. / Lamb, T. R. | SAE Technical Papers | 1981



    Application of Fuzzy Logic to Rotorcraft AFCS

    Sherman / American Helicopter Society | British Library Conference Proceedings | 1993


    A study of (AFCS) communications measurement program

    Breipohl, A.M. / Shanmugam, K.S. / Doemland, H. | Tema Archive | 1973


    Advanced AFCS developments on the XV-15 tilt rotor research aircraft

    Churchill, G. B. / Gerdes, R. M. | NTRS | 1984