|
|
 |
|
Informal Formal Methods Seminar by Andre Galdino |
|
Date: July 28, 2006
Time: 10:30am
Location: NIA, Rm 137
An Optimal 2-D Conflict Resolution Algorithm
Andre Galdino, University of Brazilia
Highly accurate positioning systems and new broadcasting technology have enabled air traffic management concepts where the responsibility for aircraft separation resides on pilots rather than on air traffic controllers. Recently, the Formal Methods Group at NIA and NASA Langley Research Center has proposed and formally verified an algorithm, called RR3D, for distributed three dimensional conflict resolution and recovery. RR3D computes resolution maneuvers where only one parameter of the aircraft, i.e., ground speed, vertical speed, or ground tracking, is modified. These kinds of maneuvers are simple to implement by a pilot. However, they are not necessarily optimal from a geometrical point of view. Indeed, optimal resolutions generally require the combination of all the parameters of the aircraft. So, we propose a two dimensional resolution and recovery algorithm, called RR2D, that computes resolution maneuvers that are optimal with respect to ground speed and ground tracking changes. The algorithm has been formally verified in the Prototype Verification System (PVS).
|
|
|
Home