NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login

Press Enter or click the Search button to begin your search.

Back to Results
Formal Analysis of the Compact Position Reporting AlgorithmThis presentation documents the formal analysis of the compact position reporting (CPR) algorithm. CPR is a fundamental part of Automatic Dependent Surveillance - Broadcast (ADS-B), which is a global protocol for aircraft communication. The formal analysis found and corrected issues with the algorithm, proposed simplifications, and created a formally verified reference implementation, all of which are incorporated in the governing standards document.
Document ID
20220009508
Acquisition Source
Langley Research Center
Document Type
Presentation
Authors
Aaron Dutle (Langley Research Center Hampton, Virginia, United States)
César Muñoz (Langley Research Center Hampton, Virginia, United States)
Laura Titolo (National Institute of Aerospace Hampton, Virginia, United States)
Mariano Moscato (National Institute for Aerospace Technology Madrid, Spain)
Gregory Anderson (University of Virginia Charlottesville, Virginia, United States)
François Bobot (French Alternative Energies and Atomic Energy Commission Palaiseau, France)
Date Acquired
June 17, 2022
Subject Category
Computer Programming And Software
Meeting Information
Meeting: System-Wide Safety TC-3 Workshop
Location: Virtual
Country: US
Start Date: July 12, 2022
End Date: July 13, 2022
Sponsors: National Aeronautics and Space Administration
Funding Number(s)
WBS: 3400428.02.20.07.01
Distribution Limits
Public
Copyright
Portions of document may include copyright protected material.
Technical Review
NASA Peer Committee
Keywords
Formal Methods
ADS-B

Related Records

There are no records associated with this record.
No Preview Available