Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Verifying an Aircraft Proximity Characterization Method in Coq
verfasst von : Dongxi Liu, Neale L. Fulton, John Zic, Martin de Groot
Erschienen in: Formal Methods and Software Engineering
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In this paper, we present a verification of an aircraft proximity characterization method in the proof assistant Coq. Our verification covers aircraft kinematics, foundational geometric objects, and real analysis, which are all used in the proximity characterization method. These subjects from different areas make our verification complicated. Through the verification, all proximity characteristics in that method are formalized and provided with machine-checkable proofs. We have identified and corrected several mistakes in the informal description of the method, and improved the accuracy of proximity characteristics by explicitly defining their conditions in the formalization. Our verification shows the effectiveness of using Coq to increase the trust to the aircraft proximity characterization method.