Background:
Intelligent aerospace systems of the future will be smarter and self-sufficient in terms of self-healing, self-diagnosis, and self-navigation. An unprecedented amount of real-time will be available to both manned and unmanned aircraft systems (UAS) from local sources like onboard sensors and remote sources like other aircraft, ground-stations and satellites. Dynamic data-driven application system paradigms can be implemented to use this data for various types of mission-criticlaand safety-critical aerospace applications like collaborative flight-planning and weather-aware navigation.
Formal methods allow the verification of safety-critical systems by using tools such as model checking and theorem proving. The main goal of this project is to integrate the use of formal verification techniques in the runtime architecture of dynamic data-driven applications systems and the development of proof libraries for easy verification of higher-level statistical and stochastic properties of such systems.
This project is a part of the ASSURE research program at the Worldwide Computing Laboratory (WCL), Rensselaer Polytechnic Institute.
Goals:
- Runtime integration of formal methods and DDDAS
- Development of dedicated proof libraries that can be reused for verification of cyber-physical aerospace systems
Publications:
Open Source Software/Formal Proofs:
- Our extension to the Athena proof library for DDDAS
- Our Agda Libraries for Safety Envelopes (DDDAS) (version: 0.1.2.0) (Older versions: 0.1.1.0)
Videos/Demo:
- A simulation of safety envelopes using synthetized data. The green regions correspond to values that belong to the safety envelope. The simulation shows a fixed airspeed of 8.70 m/s and angle of attack variable (increasing from 1º to 16º).
- Safety envelopes simulation using synthetized data. Fixed angle of attack of 11.5º and variable airspeed (from 17 to 1 m/s).
- A simulation of the Formal DDDAS Feedback Loop presented in our DDDAS 2020 paper using synthetic data.