m (Scipediacontent moved page Draft Content 140649507 to Galdino et al 2007a) |
|||
Line 3: | Line 3: | ||
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. The Formal Methods Group at the National Institute of Aerospace and NASA Langley Research Center has proposed and formally verified an algorithm, called KB3D, for distributed three dimensional conflict resolution. KB3D computes resolution maneuvers where only one component of the velocity vector, i.e., ground speed, vertical speed, or heading, is modified. Although these maneuvers are simple to implement by a pilot, they are not necessarily optimal from a geometrical point of view. In general, optimal resolutions require the combination of all the components of the velocity vector. In this paper, we propose a two dimensional version of KB3D, which we call KB2D, that computes resolution maneuvers that are optimal with respect to ground speed and heading changes. The algorithm has been mechanically verified in the Prototype Verification System (PVS). The verification relies on algebraic proof techniques for the manipulation of the geometrical concepts relevant to the algorithm as well as standard deductive techniques available in PVS. | 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. The Formal Methods Group at the National Institute of Aerospace and NASA Langley Research Center has proposed and formally verified an algorithm, called KB3D, for distributed three dimensional conflict resolution. KB3D computes resolution maneuvers where only one component of the velocity vector, i.e., ground speed, vertical speed, or heading, is modified. Although these maneuvers are simple to implement by a pilot, they are not necessarily optimal from a geometrical point of view. In general, optimal resolutions require the combination of all the components of the velocity vector. In this paper, we propose a two dimensional version of KB3D, which we call KB2D, that computes resolution maneuvers that are optimal with respect to ground speed and heading changes. The algorithm has been mechanically verified in the Prototype Verification System (PVS). The verification relies on algebraic proof techniques for the manipulation of the geometrical concepts relevant to the algorithm as well as standard deductive techniques available in PVS. | ||
− | |||
− | |||
− | |||
− | |||
− | |||
Line 15: | Line 10: | ||
* [http://www.mat.unb.br/~ayala/KB2D.pdf http://www.mat.unb.br/~ayala/KB2D.pdf] | * [http://www.mat.unb.br/~ayala/KB2D.pdf http://www.mat.unb.br/~ayala/KB2D.pdf] | ||
+ | |||
+ | * [http://link.springer.com/content/pdf/10.1007/978-3-540-73445-1_13 http://link.springer.com/content/pdf/10.1007/978-3-540-73445-1_13], | ||
+ | : [http://dx.doi.org/10.1007/978-3-540-73445-1_13 http://dx.doi.org/10.1007/978-3-540-73445-1_13] | ||
+ | |||
+ | * [https://link.springer.com/chapter/10.1007/978-3-540-73445-1_13 https://link.springer.com/chapter/10.1007/978-3-540-73445-1_13], | ||
+ | : [http://core.ac.uk/display/24471780 http://core.ac.uk/display/24471780], | ||
+ | : [https://www.scipedia.com/public/Galdino_et_al_2007a https://www.scipedia.com/public/Galdino_et_al_2007a], | ||
+ | : [https://dblp.uni-trier.de/db/conf/wollic/wollic2007.html#GaldinoMA07 https://dblp.uni-trier.de/db/conf/wollic/wollic2007.html#GaldinoMA07], | ||
+ | : [https://www.mat.unb.br/ayala/KB2D.pdf https://www.mat.unb.br/ayala/KB2D.pdf], | ||
+ | : [https://rd.springer.com/chapter/10.1007/978-3-540-73445-1_13 https://rd.springer.com/chapter/10.1007/978-3-540-73445-1_13], | ||
+ | : [https://academic.microsoft.com/#/detail/2103285154 https://academic.microsoft.com/#/detail/2103285154] |
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. The Formal Methods Group at the National Institute of Aerospace and NASA Langley Research Center has proposed and formally verified an algorithm, called KB3D, for distributed three dimensional conflict resolution. KB3D computes resolution maneuvers where only one component of the velocity vector, i.e., ground speed, vertical speed, or heading, is modified. Although these maneuvers are simple to implement by a pilot, they are not necessarily optimal from a geometrical point of view. In general, optimal resolutions require the combination of all the components of the velocity vector. In this paper, we propose a two dimensional version of KB3D, which we call KB2D, that computes resolution maneuvers that are optimal with respect to ground speed and heading changes. The algorithm has been mechanically verified in the Prototype Verification System (PVS). The verification relies on algebraic proof techniques for the manipulation of the geometrical concepts relevant to the algorithm as well as standard deductive techniques available in PVS.
The different versions of the original document can be found in:
Published on 01/01/2007
Volume 2007, 2007
DOI: 10.1007/978-3-540-73445-1_13
Licence: CC BY-NC-SA license
Are you one of the authors of this document?