A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System

Reference. A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System

Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, André Platzer · TACAS · 2015 · dynamical-systems · DOI · pldb

Cite

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

BibTeX

bibtex · 1 line

@inbook{jeannin-2015-a, title={A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System}, ISBN={9783662466810}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-662-46681-0_2}, DOI={10.1007/978-3-662-46681-0_2}, booktitle={Tools and Algorithms for the Construction and Analysis of Systems}, publisher={Springer Berlin Heidelberg}, author={Jeannin, Jean-Baptiste and Ghorbal, Khalil and Kouskoulas, Yanni and Gardner, Ryan and Schmidt, Aurora and Zawadzki, Erik and Platzer, André}, year={2015}, pages={21–36} }

hayagriva YAML (typst)

yaml · 22 lines

jeannin-2015-a:
  type: chapter
  title: A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System
  author:
  - Jeannin, Jean-Baptiste
  - Ghorbal, Khalil
  - Kouskoulas, Yanni
  - Gardner, Ryan
  - Schmidt, Aurora
  - Zawadzki, Erik
  - Platzer, André
  date: 2015
  page-range: 21-36
  url: http://dx.doi.org/10.1007/978-3-662-46681-0_2
  serial-number:
    doi: 10.1007/978-3-662-46681-0_2
    isbn: '9783662466810'
    issn: 1611-3349
  parent:
    type: book
    title: Tools and Algorithms for the Construction and Analysis of Systems
    publisher: Springer Berlin Heidelberg

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

Cited by (2)

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

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

DOI

Cites 22 works (0 here)

External (22)

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)
A formally verified hybrid system for the next-generation airborne collision avoidance system (Tech. Rep. CMU-CS-14-138) (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, MIT Lincoln Laboratory) (2009)
Differential Dynamic Logic for Hybrid Systems (2008)
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) (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)