In the next 20 years the airspace traffic will increase by 4 times, and current technology is not going to be able to guarantee an acceptable level of safety, reliability, and security.

The NextGen project aims to solve this problem, and define a more advanced an capable Air Traffic Control System. Such a huge project requires a wide set of different analysis, including political and environmental impact, cost analysis, useability, safety and reliability analysis, and so on. The project that we present here provides an overview of the formal analysis applied to the Automated Air Traffic Control Designs, in order to evaluate the different possible approaches.

Publications

• Comparing Different Functional Allocations in Automated Air Traffic Control Design
  Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta, and Kristin Y. Rozier. FMCAD2015.
• Model Checking at Scale: Automated Air Traffic Control Design Space Exploration
  Marco Gario , Alessandro Cimatti , Cristian Mattarei , Stefano Tonetta , and Kristin Yvonne Rozier. CAV2016.