In the early phases of the design of safety-critical systems, we need the ability to analyze the safety of different design solutions, comparing how different functional allocations impact the overall reliability of the system. To achieve this goal, we can apply formal techniques ranging from model checking to model-based fault-tree analysis. Using the results of the verification and safety analysis, we can compare different solutions and provide the domain experts with information on the strengths and weaknesses of each solution. In this paper, we consider NASA's early designs and functional allocation hypotheses for the next air traffic control system for the United States. In particular, we consider how the allocation of separation assurance capabilities and the required communication between agents affects the safety of the overall system. Due to the high level of details, we need to abstract the domain while retaining all of the key properties of NASA's designs. We present the modeling approach and verification process that we adopted. Finally, we discuss the results of the analysis when comparing different configurations including both new, self-separating and traditional, ground-separated aircraft.

Comparing Different Functional Allocations in Automated Air Traffic Control Design

Mattarei, Cristian;Cimatti, Alessandro;Gario, Marco Elio Gustavo;Tonetta, Stefano;
2015

Abstract

In the early phases of the design of safety-critical systems, we need the ability to analyze the safety of different design solutions, comparing how different functional allocations impact the overall reliability of the system. To achieve this goal, we can apply formal techniques ranging from model checking to model-based fault-tree analysis. Using the results of the verification and safety analysis, we can compare different solutions and provide the domain experts with information on the strengths and weaknesses of each solution. In this paper, we consider NASA's early designs and functional allocation hypotheses for the next air traffic control system for the United States. In particular, we consider how the allocation of separation assurance capabilities and the required communication between agents affects the safety of the overall system. Due to the high level of details, we need to abstract the domain while retaining all of the key properties of NASA's designs. We present the modeling approach and verification process that we adopted. Finally, we discuss the results of the analysis when comparing different configurations including both new, self-separating and traditional, ground-separated aircraft.
978-0-9835678-5-1
File in questo prodotto:
File Dimensione Formato  
main.pdf

non disponibili

Descrizione: Camera Ready - PDF
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 705.11 kB
Formato Adobe PDF
705.11 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/303423
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact