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.
- Runtime integration of formal methods and DDDAS
- Development of dedicated proof libraries that can be reused for verification of cyber-physical aerospace systems