Elkin Cruz-Camacho,
Ahmad Amer,
Fotis Kopsaftopoulos,
and Carlos A. Varela.
Formal Safety Envelopes for Provably Accurate State Classification by Data-Driven Flight Models.
Journal of Aerospace Information Systems,
20(1):3-16,
2023.
Keyword(s): Formal verification,
Agda,
Safety envelopes,
Runtime verification,
dddas.
Abstract: |
We present a novel approach to formally verify data-driven models for state classification in the domain of aerospace. Dynamic data-driven application systems (DDDAS) extend first-principles models with dynamically sensed data enabling the diagnosis and healing of aircrafts during flight. The intrinsic complexity of these systems makes them prone to spurious errors caused by unseen conditions. Formal (software) verification is a technique that goes beyond unit testing or statistical model checking, which can only guarantee system correctness over a fraction of the system's input space. {\em Safety envelopes} bound regions of the system's input space where a formal proof of correctness of state classification holds. We focus on two questions for defining safety envelope boundaries: ({\em i}) does the data follow the model? and ({\em ii}) what is the most likely state of the system given the data? We evaluate safety envelopes with data derived from a wind tunnel experiment tackling the problem of stall detection given piezo-electric sensor measurements over a wing's skin. We define tailored metrics to show the quality of different data-driven models. We encode safety envelopes in the proof assistant Agda, and illustrate their applicability across a variety of input dimensions and Gaussian Process Regression Model (GPRM)-generated data. |
@ARTICLE{cruz-jais-2023,
AUTHOR = {Elkin Cruz-Camacho and Ahmad Amer and Fotis Kopsaftopoulos and Carlos A. Varela},
JOURNAL = {Journal of Aerospace Information Systems},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {1},
PAGES = {3--16},
PUBLISHER = {American Institute of Aeronautics and Astronautics},
TITLE = {Formal Safety Envelopes for Provably Accurate State Classification by Data-Driven Flight Models},
VOLUME = {20},
YEAR = {2023},
ABSTRACT = {We present a novel approach to formally verify data-driven models for state classification in the domain of aerospace. Dynamic data-driven application systems (DDDAS) extend first-principles models with dynamically sensed data enabling the diagnosis and healing of aircrafts during flight. The intrinsic complexity of these systems makes them prone to spurious errors caused by unseen conditions. Formal (software) verification is a technique that goes beyond unit testing or statistical model checking, which can only guarantee system correctness over a fraction of the system's input space. {\em Safety envelopes} bound regions of the system's input space where a formal proof of correctness of state classification holds. We focus on two questions for defining safety envelope boundaries: ({\em i}) does the data follow the model? and ({\em ii}) what is the most likely state of the system given the data? We evaluate safety envelopes with data derived from a wind tunnel experiment tackling the problem of stall detection given piezo-electric sensor measurements over a wing's skin. We define tailored metrics to show the quality of different data-driven models. We encode safety envelopes in the proof assistant Agda, and illustrate their applicability across a variety of input dimensions and Gaussian Process Regression Model (GPRM)-generated data.},
DOI = {https://doi.org/10.2514/1.I011073},
OPTISBN = {},
OPTISSN = {},
KEYWORDS = {Formal verification, Agda, Safety envelopes, Runtime verification, dddas},
OPTURL = {},
OPTURL-PUBLISHER = {},
PDF = {http://wcl.cs.rpi.edu/papers/cruz-jais-2022.pdf}
}
Saswata Paul,
Elkin Cruz,
Airin Dutta,
Ankita Bhaumik,
Erik Blasch,
Gul Agha,
Stacy Patterson,
Fotis Kopsaftopoulos,
and Carlos Varela.
Formal Verification of Safety-Critical Aerospace Systems.
IEEE Aerospace and Electronic Systems Magazine,
38(5):72-88,
2023.
Keyword(s): theorem proving,
runtime verification,
stochastic systems,
distributed systems.
Abstract: |
Developments in autonomous aircraft, such as electrical vertical take-off and landing vehicles and multicopter drones, raise safety-critical concerns in populated areas. This article presents the Analysis of Safety-Critical Systems Using Formal Methods-Based Runtime Evaluation (ASSURE) framework, which is a collection of techniques for aiding in the formal verification of safety-critical aerospace systems. ASSURE supports the rigorous verification of deterministic and nondeterministic properties of both distributed and centralized aerospace applications by using formal theorem proving tools. We present verifiable algorithms and software, formal reasoning models, formal proof libraries, and a data-driven runtime verification approach for aerospace systems toward a provably safe Internet of Planes infrastructure. |
@ARTICLE{paul_2023_aesm,
AUTHOR = {Saswata Paul and Elkin Cruz and Airin Dutta and Ankita Bhaumik and Erik Blasch and Gul Agha and Stacy Patterson and Fotis Kopsaftopoulos and Carlos Varela},
JOURNAL = {IEEE Aerospace and Electronic Systems Magazine},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {5},
PAGES = {72-88},
TITLE = {Formal Verification of Safety-Critical Aerospace Systems},
VOLUME = {38},
ABSTRACT = {Developments in autonomous aircraft, such as electrical vertical take-off and landing vehicles and multicopter drones, raise safety-critical concerns in populated areas. This article presents the Analysis of Safety-Critical Systems Using Formal Methods-Based Runtime Evaluation (ASSURE) framework, which is a collection of techniques for aiding in the formal verification of safety-critical aerospace systems. ASSURE supports the rigorous verification of deterministic and nondeterministic properties of both distributed and centralized aerospace applications by using formal theorem proving tools. We present verifiable algorithms and software, formal reasoning models, formal proof libraries, and a data-driven runtime verification approach for aerospace systems toward a provably safe Internet of Planes infrastructure.},
YEAR = {2023},
OPTABSTRACT = {},
DOI = {https://doi.org/10.1109/MAES.2023.3238378},
OPTISBN = {},
OPTISSN = {},
keywords = {theorem proving, runtime verification, stochastic systems, distributed systems},
OPTKEYWORDS = {},
OPTURL = {},
OPTURL-PUBLISHER = {},
PDF = {http://wcl.cs.rpi.edu/papers/paul_2023_aesm.pdf}
}