Formal Analysis of Air Traffic Management Systems
The research has focused on fundamental algorithms for conflict detection
and resolution (CD&R). The goal is
to formally prove that the safety-critical algorithms produce valid solutions
that are guaranteed to maintain separation under all possible scenarios.
Current research has assumed perfect knowledge of the location of other
aircraft in the vacinity so absolute guarantees are possible. Future work
will look at the system design issues associated with possibly incomplete
or faulty information from communication sources.