Intelligent aerospace systems of the future are expected to be “smarter” and more self-sufficient in terms of self-diagnosis, self-healing, self-navigation, and overall situational awareness. Enhanced situational awareness will be facilitated by access to a vast amount of real-time data from on-board sensors, other aircraft, ground stations, and satellites, as well as contextual models from environment analysis of weather, terrain, and structures. The Dynamic data-driven application systems (DDDAS) paradigm incorporates real-time data for creating high-fidelity models to aid in flight-diagnosis and decision-making. DDDAS techniques accommodate the fusion of dynamic-data, algorithms, computation, and interpretation, making them apposite for use in safety-critical intelligent sensing systems. In safety-critical systems, it is important to have irrefutable system assurance over hardware and software guarantees. Formal methods allow the development of machine-checked correctness proofs for such guarantees, facilitating the verification of such systems on infinite states. This chapter presents formal correctness envelopes (FCE), analogous to performance envelopes of an aircraft, which represent the operating conditions under which the guarantees regarding a system’s properties hold. FCEs are data-driven, allowing them to be computed, quantified, and monitored in real-time using correctness sentinels. Correctness sentinels are executable programs that use the notion of correctness envelopes to monitor real-time data-streams and detect the status of a system’s state with respect to relevant envelopes during runtime. At any given point of time, correctness sentinels can provide useful information about which system properties can be guaranteed and with how much confidence. FCEs, in tandem with correctness sentinels, allow the development of aerospace systems that can monitor formal guarantees in real-time and dynamically adapt to remain within the bounds of those guarantees.
Reference
invited chapter, Frederica Darema and Erik Blasch, editors, Handbook of Dynamic Data-Driven Application Systems. Springer, 2021.
Bibtex
@article{paultowards,
title={Towards Formal Correctness Envelopes for Dynamic Data-Driven Aerospace Systems},
author={Paul, Saswata and Patterson, Stacy and Kopsaftopoulos, Fotis and Varela, Carlos}
}