Galdino et al 2007a - Revision history

Scipediacontent at 13:37, 21 January 2021

2021-01-21T13:37:36Z

Scipediacontent: Scipediacontent moved page Draft Content 140649507 to Galdino et al 2007a

2020-10-14T12:14:26Z

Scipediacontent moved page Draft Content 140649507 to Galdino et al 2007a

Scipediacontent: Created page with " == Abstract == Highly accurate positioning systems and new broadcasting technology have enabled air traffic management concepts where the responsibility for aircraft separat..."

2020-10-14T12:14:23Z

Created page with " == Abstract == Highly accurate positioning systems and new broadcasting technology have enabled air traffic management concepts where the responsibility for aircraft separat..."

New page

== Abstract ==

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.

Document type: Part of book or chapter of book

== Full document ==
<pdf>Media:Draft_Content_140649507-beopen493-1250-document.pdf</pdf>

== Original document ==

The different versions of the original document can be found in:

* [http://www.mat.unb.br/~ayala/KB2D.pdf http://www.mat.unb.br/~ayala/KB2D.pdf]

← Older revision		Revision as of 13:37, 21 January 2021
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.
−
−	~~Document type: Part of book or chapter of book~~
−
−	~~== Full document ==~~
−	~~<pdf>Media:Draft_Content_140649507-beopen493-1250-document.pdf</pdf>~~


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]

← Older revision	Revision as of 12:14, 14 October 2020
(No difference)