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

Autor:	André Platzer, Yanni Kouskoulas, Erik Zawadzki, Khalil Ghorbal, Aurora Schmidt, Ryan W. Gardner, Jean-Baptiste Jeannin
Rok vydání:	2015
Předmět:	Airborne collision avoidance system Set (abstract data type) Automated theorem proving Computer science Aviation business.industry Hybrid system Markov decision process business Advice (complexity) Simulation Collision avoidance Reliability engineering
Zdroj:	Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783662466803 TACAS
DOI:	10.1007/978-3-662-46681-0_2
Popis:	The Next-Generation Airborne Collision Avoidance System ACASi¾?X is intended to be installed on all large aircraft to give advice to pilots and prevent mid-air collisions with other aircraft. It is currently being developed by the Federal Aviation Administration FAA. In this paper we determine the geometric configurations under which the advice given by ACAS X is safe under a precise set of assumptions and formally verify these configurations using hybrid systems theorem proving techniques. We conduct an initial examination of the current version of the real ACAS X system and discuss some cases where our safety theorem conflicts with the actual advisory given by that version, demonstrating how formal, hybrid approaches are helping ensure the safety of ACAS X. Our approach is general and could also be used to identify unsafe advice issued by other collision avoidance systems or confirm their safety.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::61d1b3af22b253fa95a73dbf00bffce0 https://doi.org/10.1007/978-3-662-46681-0_2 Zobrazit plný text záznamu