Verifying Safety of NextGen Models

The goal of NASA’s NextGen research is to accommodate the traffic increase coming over the 15 years. One requirement for NextGen is to provide a better, at least the same, level of safety system, compared to the current ATS (Air transportation System). Using the Brahms Multi Agent System Modeling framework, researchers at NASA and the FAA are building models describing actions of flight and ground staff. These models are being explored to find better ways to coordinate to keep planes in the air, as well as how to land them quicker and safer.

Within those models, the Java Pathfinder tool has been used to verify properties related to safety and workload. This verification process suffers from the (in)famous state space explosion problem: for the large model it is not possible to do complete state space exploration.

In this proposal we propose to use the GALE optimizer (GALE is a fast heuristic algorithm which can find the optimal result to the multi-objectives problem by pruning the unpromising subspace) to find the most promising sub-state space in the models so that the verification process can be targeted and more efficient.