Aerospace systems are inherently stochastic and increasingly data-driven, thus hard to formally verify. Data-driven statistical models can be used to estimate the state and classify potentially anomalous conditions of aerospace systems from multiple heterogeneous sensors with high accuracy. In this paper, we consider the problem of precisely bounding the regions in the sensor input space of a stochastic system in which safe state classification can be formally proven. As an archetypal application, we consider a statistical model created to detect aerodynamic stall in a prototype wing retrofitted with piezoelectric sensors and used to generate data in a wind tunnel for different flight states. We formally define safety envelopes as regions parameterized by z and τ , to respectively capture how model-predictable observed sensor values are, and given these values, how likely the model’s accurate state classification is. Safety envelopes are formalized in the Agda proof assistant, used to also generate formally verified runtime monitors for sensor data stream analyses in the Haskell programming language. We further propose a new metric for model classification quality, evaluate it on our wing prototype model, and compare it to the model restricted to two different fixed airspeeds, and enhanced to a continuous Gaussian process regression model. Safety envelopes are an important step in formally verifying precise probabilistic properties of data-driven models used in stochastic aerospace systems and could be used by advanced control algorithms to maintain these systems well within safe operation boundaries.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal Safety Envelopes for Provably Accurate State Classification by Data-Driven Flight Models


    Contributors:

    Published in:

    Publication date :

    2022-12-15


    Size :

    14 pages




    Type of media :

    Article (Journal)


    Type of material :

    Electronic Resource


    Language :

    English



    Provably Correct Safety Protocol for Cooperative Platooning

    Mair, Sebastian / Althoff, Matthias | IEEE | 2024


    Envelopes for Flight Through Stochastic Gusts

    Richardson, J R | Online Contents | 2013


    Envelopes for Flight Through Stochastic Gusts

    Richardson, J. / Atkins, E. / Kabamba, P. et al. | British Library Conference Proceedings | 2011


    Envelopes for Flight Through Stochastic Gusts

    Richardson, J. / Atkins, E. / Kabamba, P. et al. | British Library Conference Proceedings | 2011


    Envelopes for Flight Through Stochastic Gusts

    Richardson, Johnhenri R. / Atkins, Ella M. / Kabamba, Pierre T. et al. | AIAA | 2013