Motivation
The failure or malfunction of safety-critical aerospace, healthcare, power generation, and transportation systems can have catastrophic consequences for human beings and the environment. This makes it necessary to verify and validate such critical systems in order to guarantee their safe operation. Formal methods can facilitate the rigorous verification of such systems by using mathematical techniques to reason about the properties of the underlying hardware and software components. The ASSURE research program aims to employ formal methods-based techniques for the verification of safety-critical systems and their correctness properties.
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 is a joint effort with Prof. Carlos Varela from the Computer Science Department at RPI.
For more info please see: http://wcl.cs.rpi.edu/pilots/fvdddas/
Objectives
- Runtime integration of formal methods and DDDAS
- Development of dedicated proof libraries that can be reused for verification of cyber-physical aerospace systems
