A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system

Reference. A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system

Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora Schmidt, Ryan Gardner, Stefan Mitsch, André Platzer · STTT · 2016 · dynamical-systems · DOI

Cite

Cite as @jeannin-2016-a (helia, typst) · \cite{jeannin-2016-a} (LaTeX)

BibTeX

bibtex · 1 line

@article{jeannin-2016-a, title={A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system}, volume={19}, ISSN={1433-2787}, url={http://dx.doi.org/10.1007/s10009-016-0434-1}, DOI={10.1007/s10009-016-0434-1}, number={6}, journal={International Journal on Software Tools for Technology Transfer}, publisher={Springer Science and Business Media LLC}, author={Jeannin, Jean-Baptiste and Ghorbal, Khalil and Kouskoulas, Yanni and Schmidt, Aurora and Gardner, Ryan and Mitsch, Stefan and Platzer, André}, year={2016}, month=Oct, pages={717–741} }

hayagriva YAML (typst)

yaml · 23 lines

jeannin-2016-a:
  type: article
  title: A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system
  author:
  - Jeannin, Jean-Baptiste
  - Ghorbal, Khalil
  - Kouskoulas, Yanni
  - Schmidt, Aurora
  - Gardner, Ryan
  - Mitsch, Stefan
  - Platzer, André
  date: 2016-10
  page-range: 717-741
  url: http://dx.doi.org/10.1007/s10009-016-0434-1
  serial-number:
    doi: 10.1007/s10009-016-0434-1
    issn: 1433-2787
  parent:
    type: periodical
    title: International Journal on Software Tools for Technology Transfer
    publisher: Springer Science, Business Media LLC
    issue: 6
    volume: 19

Download: jeannin-2016-a.bib · jeannin-2016-a.yml

Cited by (2)

Provably Safe Optimization of Arrival Flows Into Terminal Airspace dane-2026-provablyAIAA AVIATION 2026 Forum · 2026

DOI

Automating Geometric Proofs of Collision Avoidance with Active Corners kheterpal-2022-automatingFMCAD · 2022

Avoiding collisions between obstacles and vehicles such as cars, robots or aircraft is essential to the development of automation and autonomy. To simplify the problem, many collision avoidance algorithms and proofs consider vehicles to be a point mass, though the actual vehicles are not points. In this paper, we consider a convex polygonal vehicle with nonzero area traveling along a 2-dimensional trajectory. We derive an easily-checkable, quantifier-free formula to check whether a given obstacle will collide with the vehicle moving on the planned trajectory. We apply our method to two case studies of aircraft collision avoidance and study its performance.

DOI · arXiv

Cites 25 works (1 here)

With notes (1)

A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System jeannin-2015-aTACAS · 2015

DOI · pldb

External (24)

Automated Deduction - CADE-25 (proceedings, eds. Felty & Middeldorp) (2015)
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (2015)
A Uniform Substitution Calculus for Differential Dynamic Logic (2015)
Analyzing the Next Generation Airborne Collision Avoidance System (2014)
Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges (2014)
Algorithm design description for the surveillance and tracking module of ACAS X (2014)
Algorithm design description for the threat resolution module of ACAS X (2014)
Optimizing the Next Generation Collision Avoidance System for Safe, Suitable, and Acceptable Operational Performance (2013)
Compression of Optimal Value Functions for Markov Decision Processes (2013)
Formal verification of distributed aircraft controllers (2013)
Logics of Dynamical Systems (2012)
Next generation airborne collision avoidance system (2012)
Introduction to TCAS II, version 7.1 (2011)
Logical Analysis of Hybrid Systems (2010)
Robust airborne collision avoidance through dynamic programming (Tech. Rep. ATC-371) (2010)
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study (2009)
Evaluation of TCAS II version 7.1 using the FAA fast-time encounter generator model (Tech. Rep. ATC-346) (2009)
Differential Dynamic Logic for Hybrid Systems (2008)
Correlated encounter model for cooperative aircraft in the national airspace system version 1.0 (Tech. Rep. ATC-344) (2008)
Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm (2007)
Provably Safe Coordinated Strategy for Distributed Conflict Resolution (2005)
Conflict resolution for air traffic management: a study in multiagent hybrid systems (1998)
On the formal verification of the TCAS conflict resolution algorithms (1997)
Quantifier elimination for real closed fields by cylindrical algebraic decomposition (1975)