Skip to main content
Top
Published in: International Journal on Software Tools for Technology Transfer 2/2016

01-04-2016 | TACAS 2014

Probabilistic verification and synthesis of the next generation airborne collision avoidance system

Authors: Christian von Essen, Dimitra Giannakopoulou

Published in: International Journal on Software Tools for Technology Transfer | Issue 2/2016

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

The next generation airborne collision avoidance system, ACAS X, departs from the traditional deterministic model on which the current system, TCAS, is based. To increase robustness, ACAS X relies on probabilistic models to represent the various sources of uncertainty. The work reported in this paper identifies verification challenges for ACAS X, and studies the applicability of probabilistic verification and synthesis techniques in addressing these challenges. Due to shortcomings of off-the-shelf probabilistic analysis tools, we developed a new framework, named VeriCA (Verification for Collision Avoidance). VeriCA is a combined probabilistic synthesis and verification framework that is custom designed for ACAS X and systems with similar characteristics. VeriCA supports Java as a modeling language, is memory efficient, employs parallelization, and provides an interactive simulator that displays aircraft encounters and the corresponding ACAS X behavior. We describe the application of our framework to ACAS X, together with the results and recommendations that our analysis produced.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

Footnotes
1
As explained in [9], the advisory response is determined according to a Bernoulli process, so the delay until response follows a geometric distribution. If the response probability at each step in the process is \(\frac{1}{1+k}\), then the mean time until response is k.
 
Literature
1.
go back to reference Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: STACS 2006, 23rd Annual Symposium on Theoretical Aspects of Computer Science, Marseille, France, February 23–25, 2006, pp. 325–336 (2006) Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: STACS 2006, 23rd Annual Symposium on Theoretical Aspects of Computer Science, Marseille, France, February 23–25, 2006, pp. 325–336 (2006)
2.
go back to reference Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA’12), volume 7561 of LNCS, pp. 317–332. Springer (2012) Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA’12), volume 7561 of LNCS, pp. 317–332. Springer (2012)
3.
go back to reference Galdino, A.L., Muñoz, C., Ayala-Rincón, M.: Formal verification of an optimal air traffic conflict resolution and recovery algorithm. In: Logic, Language, Information and Computation, 14th International Workshop, WoLLIC 2007, Rio de Janeiro, Brazil, July 2–5, 2007, pp. 177–188 (2007) Galdino, A.L., Muñoz, C., Ayala-Rincón, M.: Formal verification of an optimal air traffic conflict resolution and recovery algorithm. In: Logic, Language, Information and Computation, 14th International Workshop, WoLLIC 2007, Rio de Janeiro, Brazil, July 2–5, 2007, pp. 177–188 (2007)
4.
go back to reference 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
5.
go back to reference Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comp. 6, 102–111 (1994)MATH Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comp. 6, 102–111 (1994)MATH
6.
go back to reference Jeannin, J., 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: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11–18, 2015, pp. 21–36 (2015) Jeannin, J., 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: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11–18, 2015, pp. 21–36 (2015)
7.
go back to reference Julier, S.J., Uhlmann, J.K.: Unscented filtering and nonlinear estimation. Proc. IEEE 92(3), 401–422 (2004)CrossRef Julier, S.J., Uhlmann, J.K.: Unscented filtering and nonlinear estimation. Proc. IEEE 92(3), 401–422 (2004)CrossRef
8.
go back to reference Katoen, J., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90–104 (2011)CrossRef Katoen, J., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90–104 (2011)CrossRef
9.
go back to reference Kochenderfer, M.J.: Decision making under uncertainty: theory and application. MIT Press, Cambridge (2015). Please cehck and confirm the publisher location is correct and amend if necessaryMATH Kochenderfer, M.J.: Decision making under uncertainty: theory and application. MIT Press, Cambridge (2015). Please cehck and confirm the publisher location is correct and amend if necessaryMATH
10.
go back to reference 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)
11.
go back to reference Kuchar, J., Drumm, A.C.: The traffic alert and collision avoidance system. Lincoln Lab. J. 16(2), 277 (2007) Kuchar, J., Drumm, A.C.: The traffic alert and collision avoidance system. Lincoln Lab. J. 16(2), 277 (2007)
12.
go back to reference Kwiatkowska, M.Z., Norman, G., Parker. D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14–20, 2011, pp. 585–591 (2011) Kwiatkowska, M.Z., Norman, G., Parker. D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14–20, 2011, pp. 585–591 (2011)
13.
go back to reference 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, April 8–11, 2013, Philadelphia, PA, USA, 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, April 8–11, 2013, Philadelphia, PA, USA, pp. 125–130 (2013)
14.
go back to reference 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)
15.
go back to reference Platzer, A., Clarke E.M.: Formal verification of curved flight collision avoidance maneuvers: A case study. In: FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2–6, 2009, pp. 547–562 (2009) Platzer, A., Clarke E.M.: Formal verification of curved flight collision avoidance maneuvers: A case study. In: FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2–6, 2009, pp. 547–562 (2009)
16.
go back to reference Rennen, G., van Dam, E.R., den Hertog, D.: Enhancement of sandwich algorithms for approximating higher-dimensional convex Pareto sets. INFORMS J. Comp. 23(4), 493–517 (2011)MathSciNetCrossRefMATH Rennen, G., van Dam, E.R., den Hertog, D.: Enhancement of sandwich algorithms for approximating higher-dimensional convex Pareto sets. INFORMS J. Comp. 23(4), 493–517 (2011)MathSciNetCrossRefMATH
17.
go back to reference Tomlin, C., Pappas, G.J., Sastry, S.: Conflict resolution for air traffic management: A study in multiagent hybrid systems. IEEE Trans. Auto. Cont. 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. Auto. Cont. 43(4), 509–521 (1998)MathSciNetCrossRefMATH
18.
go back to reference von Essen C.: Quantitative Verification and Synthesis. PhD Thesis, Université Joseph Fourier, Grenoble, France (2014) von Essen C.: Quantitative Verification and Synthesis. PhD Thesis, Université Joseph Fourier, Grenoble, France (2014)
19.
go back to reference von Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014, pp. 620–635 (2014) von Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014, pp. 620–635 (2014)
20.
go back to reference Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods Syst. Design 43(2), 338–367 (2013)CrossRefMATH Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods Syst. Design 43(2), 338–367 (2013)CrossRefMATH
Metadata
Title
Probabilistic verification and synthesis of the next generation airborne collision avoidance system
Authors
Christian von Essen
Dimitra Giannakopoulou
Publication date
01-04-2016
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 2/2016
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-015-0388-8

Other articles of this Issue 2/2016

International Journal on Software Tools for Technology Transfer 2/2016 Go to the issue

Premium Partner