In the next 20 years the airspace traffic will increase by 4 times, and current technology cannot guarantee an acceptable level of safety, reliability, and security. NASA is evaluating different options to design a more advanced and capable Air Traffic Control System. Such a huge project requires a wide range of different analysis, including political and environmental impact, cost analysis, usability, safety and reliability analysis, and so on.
The collaboration between NASA and FBK focused on the application of formal techniques to analyze the Automated Air Traffic Control design space, in order to evaluate and compare different design options. In collaboration with NASA experts, we focused on the problem of Functional Allocation, i.e., how to delegate separation of aircraft between on-board and on-ground components. We identified several design choices and trade-offs that lead to a design space with more than 1600 solutions. By applying a compositional design approach, each of them was exhaustively analyze in terms of properties satisfaction, safety assessment and reliability. The results were discussed and validated by NASA and highlighted novel and well-known issues.
(More details and materials on the project are available on the dedicated website)
