Formal Verification of Dynamic Data-Driven Applications Systems

HTML5 Icon

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 was conceived at the Worldwide Computing Laboratory (WCL), Rensselaer Polytechnic Institute, as a child project of the PILOTS programming language.

Goals:

Publications:

Open Source Software/Formal Proofs:

Comments/suggestions/patches are welcome!