Skip to main content

2016 | OriginalPaper | Buchkapitel

Exploring Model Quality for ACAS X

verfasst von : Dimitra Giannakopoulou, Dennis Guck, Johann Schumann

Erschienen in: FM 2016: Formal Methods

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

The next generation airborne collision avoidance system, ACAS X, aims to provide robustness through a probabilistic model that represents sources of uncertainty. From this model, dynamic programming produces a look-up table that is used to give advisories to the pilot in real time. The model is not present in the final system and is therefore not included in the standard certification processes. Rather, the model is checked indirectly, by ensuring that ACAS X performs as well as, or better than, the state-of-the-art, TCAS. We claim that to build confidence in such systems, it is important to target model quality directly. We investigate this issue of model quality as part of our research on informing certification standards for autonomy. Using ACAS X as our driving example, we study the relationship between the probabilistic model and the real world, in an attempt to characterize the quality of the model for the purpose of building ACAS X. This paper presents model conformance metrics, their application to ACAS X, and the results that we obtained from our study.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
ACAS X handles cases with multiple aircraft but this paper focuses on scenarios involving two aircraft.
 
2
We use the MDP rather than its corresponding continuous version for aircraft dynamics, because the generation of the LUT is based on the MDP model.
 
Literatur
1.
Zurück zum Zitat Dimjasevic, M., Giannakopoulou, D.: Test-case generation for runtime analysis, vice versa: verification of aircraft separation assurance. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, Baltimore, 12–17 July 2015, pp. 282–292 (2015) Dimjasevic, M., Giannakopoulou, D.: Test-case generation for runtime analysis, vice versa: verification of aircraft separation assurance. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, Baltimore, 12–17 July 2015, pp. 282–292 (2015)
2.
Zurück zum Zitat Galdino, A.L., Muñoz, C., Ayala-Rincón, M.: Formal verification of an optimal air traffic conflict resolution and recovery algorithm. In: Leivant, D., Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol. 4576, pp. 177–188. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73445-1_13 CrossRef Galdino, A.L., Muñoz, C., Ayala-Rincón, M.: Formal verification of an optimal air traffic conflict resolution and recovery algorithm. In: Leivant, D., Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol. 4576, pp. 177–188. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-73445-1_​13 CrossRef
3.
Zurück zum Zitat Ghorbal, K., Jeannin, J., Zawadzki, E., Platzer, A., Gordon, G.J., Capell, P.: Hybrid theorem proving of aerospace systems: applications and challenges. J. Aerospace Inf. Sys. 11(10), 702–713 (2014)CrossRef Ghorbal, K., Jeannin, J., Zawadzki, E., Platzer, A., Gordon, G.J., Capell, P.: Hybrid theorem proving of aerospace systems: applications and challenges. J. Aerospace Inf. Sys. 11(10), 702–713 (2014)CrossRef
4.
Zurück zum Zitat Giannakopoulou, D., Bushnell, D.H., Schumann, J., Erzberger, H., Heere, K.: Formal testing for separation assurance. Ann. Math. Artif. Intell. 63(1), 5–30 (2011)CrossRefMATH Giannakopoulou, D., Bushnell, D.H., Schumann, J., Erzberger, H., Heere, K.: Formal testing for separation assurance. Ann. Math. Artif. Intell. 63(1), 5–30 (2011)CrossRefMATH
5.
Zurück zum Zitat Giannakopoulou, D., Howar, F., Isberner, M., Lauderdale, T., Rakamaric, Z., Raman, V.: Taming test inputs for separation assurance. In: ACM/IEEE International Conference on Automated Software Engineering, ASE 2014, Vasteras, 15–19 September 2014, pp. 373–384 (2014) Giannakopoulou, D., Howar, F., Isberner, M., Lauderdale, T., Rakamaric, Z., Raman, V.: Taming test inputs for separation assurance. In: ACM/IEEE International Conference on Automated Software Engineering, ASE 2014, Vasteras, 15–19 September 2014, pp. 373–384 (2014)
6.
Zurück zum Zitat Jeannin, J.-B., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 21–36. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_2 Jeannin, J.-B., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 21–36. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46681-0_​2
7.
Zurück zum Zitat Kochenderfer, M.J.: Decision Making Under Uncertainty: Theory and Application. MIT Press, Cambridge (2015)MATH Kochenderfer, M.J.: Decision Making Under Uncertainty: Theory and Application. MIT Press, Cambridge (2015)MATH
8.
Zurück zum Zitat Kochenderfer, M.J., Chryssanthacopoulos, J.P. : Robust airborne collision avoidance through dynamic programming. Project Report ATC-371, Massachusetts Institute of Technology, Lincoln Laboratory (2011) Kochenderfer, M.J., Chryssanthacopoulos, J.P. : Robust airborne collision avoidance through dynamic programming. Project Report ATC-371, Massachusetts Institute of Technology, Lincoln Laboratory (2011)
9.
Zurück zum Zitat Kuchar, J., Drumm, A.C.: The traffic alert and collision avoidance system. Linc. Lab. J. 16(2), 277 (2007) Kuchar, J., Drumm, A.C.: The traffic alert and collision avoidance system. Linc. Lab. J. 16(2), 277 (2007)
10.
Zurück zum Zitat Lee, R., Kochenderfer, M.J., Mengshoel, O.J., Brat, G.P., Owen, M.P.: Adaptive stress testing of airborne collision avoidance systems. In: 2015 IEEE/AIAA 34th Digital Avionics Systems Conference (DASC), p. 6C2-1. IEEE (2015) Lee, R., Kochenderfer, M.J., Mengshoel, O.J., Brat, G.P., Owen, M.P.: Adaptive stress testing of airborne collision avoidance systems. In: 2015 IEEE/AIAA 34th Digital Avionics Systems Conference (DASC), p. 6C2-1. IEEE (2015)
11.
Zurück zum Zitat Loos, S.M., Renshaw, D.W., Platzer, A.: Formal verification of distributed aircraft controllers. In: Proceedings of the 16th International Conference on Hybrid systems: Computation and Control, HSCC 2013, Philadelphia, 8–11 April 2013, pp. 125–130 (2013) Loos, S.M., Renshaw, D.W., Platzer, A.: Formal verification of distributed aircraft controllers. In: Proceedings of the 16th International Conference on Hybrid systems: Computation and Control, HSCC 2013, Philadelphia, 8–11 April 2013, pp. 125–130 (2013)
12.
Zurück zum Zitat Lygeros, J., Lynch, N.: On the formal verification of the TCAS conflict resolution algorithms. In: 36th IEEE Conference on Decision and Control, pp. 1829–1834 (1997) Lygeros, J., Lynch, N.: On the formal verification of the TCAS conflict resolution algorithms. In: 36th IEEE Conference on Decision and Control, pp. 1829–1834 (1997)
13.
Zurück zum Zitat Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: a case study. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 547–562. Springer, Heidelberg (2009). doi:10.1007/978-3-642-05089-3_35 CrossRef Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: a case study. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 547–562. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-05089-3_​35 CrossRef
14.
Zurück zum Zitat Tomlin, C., Pappas, G.J., Sastry, S.: Conflict resolution for air traffic management: a study in multiagent hybrid systems. IEEE Trans. Autom. Control 43(4), 509–521 (1998)MathSciNetCrossRefMATH Tomlin, C., Pappas, G.J., Sastry, S.: Conflict resolution for air traffic management: a study in multiagent hybrid systems. IEEE Trans. Autom. Control 43(4), 509–521 (1998)MathSciNetCrossRefMATH
15.
Zurück zum Zitat Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 620–635. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_54 CrossRef Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 620–635. Springer, Heidelberg (2014). doi:10.​1007/​978-3-642-54862-8_​54 CrossRef
16.
Zurück zum Zitat von Essen, C., Giannakopoulou, D.: Probabilistic verification and synthesis of the next generation airborne collision avoidance system. STTT 18(2), 227–243 (2016)CrossRef von Essen, C., Giannakopoulou, D.: Probabilistic verification and synthesis of the next generation airborne collision avoidance system. STTT 18(2), 227–243 (2016)CrossRef
Metadaten
Titel
Exploring Model Quality for ACAS X
verfasst von
Dimitra Giannakopoulou
Dennis Guck
Johann Schumann
Copyright-Jahr
2016
DOI
https://doi.org/10.1007/978-3-319-48989-6_17