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.
D. Guck—Author performed this work while employed by SGT, Inc. as an intern at the NASA Ames Research Center.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 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.
References
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)
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
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)
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)
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)
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
Kochenderfer, M.J.: Decision Making Under Uncertainty: Theory and Application. MIT Press, Cambridge (2015)
Kochenderfer, M.J., Chryssanthacopoulos, J.P. : Robust airborne collision avoidance through dynamic programming. Project Report ATC-371, Massachusetts Institute of Technology, Lincoln Laboratory (2011)
Kuchar, J., Drumm, A.C.: The traffic alert and collision avoidance system. Linc. Lab. J. 16(2), 277 (2007)
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)
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)
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)
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
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)
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
von Essen, C., Giannakopoulou, D.: Probabilistic verification and synthesis of the next generation airborne collision avoidance system. STTT 18(2), 227–243 (2016)
Acknowledgements
We thank Ritchie Lee for his help with RLECAS, Ryan Gardner for helping us interpret the MDP, and Ryan Gardner, Mykel Kochenderfer, Ritchie Lee, and Josh Silbermann for useful discussions and for proof-reading the paper. This work was performed under the Safe Autonomous Systems Operations (SASO) project of the NASA AOSP program.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Giannakopoulou, D., Guck, D., Schumann, J. (2016). Exploring Model Quality for ACAS X. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-48989-6_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-48988-9
Online ISBN: 978-3-319-48989-6
eBook Packages: Computer ScienceComputer Science (R0)