Safety envelopes are meant to determine under which conditions and state space regions a probabilistic property of a data-driven system can be asserted with high confidence. Dynamic data-driven applications systems (DDDAS) can make use of safety envelopes to be cognizant of the formal warranties derived from their models and assumptions. An example of safety envelopes is presented as the intersection of two simpler concepts: 𝑧z-predictability and 𝜏τ-confidence; which correspond to state estimation and classification, respectively. To illustrate safety envelopes, stall detection from signal energy is shown with data gathered by piezo-electric sensors in a composite wing inside a wind tunnel under varying angles of attack and airspeed configuration. A formalization of these safety envelopes is presented in the Agda proof assistant, from which formally proven sentinel code can be generated.
Reference
International Conference on Dynamic Data Driven Application Systems, Vol. 12312, pp. 236-244, Springer, Cham, November 2020.
Bibtex
@inproceedings{cruz2020towards,
title={Towards Provably Correct Probabilistic Flight Systems},
author={Cruz-Camacho, Elkin and Paul, Saswata and Kopsaftopoulos, Fotis and Varela, Carlos A},
booktitle={International Conference on Dynamic Data Driven Application Systems},
pages={236--244},
year={2020},
organization={Springer}
}