Verifying NextGen controlling systems
The goal of NextGen research (Next Generation Air Transportation System) 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).
In this project we use the "SWAY" sampling technique to find the most promising sub-state space in the models so that the verification process can be targeted and more efficient. "SWAY" is a fast sampling technique which can find the optimal result to the multi-objectives problem by pruning the unpromising subspace. Formally, it is a response surface method that builds a heuristic approximation to different parts of the search space. When the reasoning enters each such part, rather than executing some slow and tedious evaluation step, the response surface approximation is used to score the mutations in this area.