[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

SMT-Based Aircraft Conflict Detection and Resolution

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14627))

Included in the following conference series:

  • 465 Accesses

Abstract

The integration of Unmanned Aircraft Systems (UAS) in the National Airspace System (NAS) for Urban Air Mobility (UAM) operations will create the need to develop robust, efficient, and verifiable tools and techniques for UAS Traffic Management (UTM). In this paper, we present a novel approach for strategic detection and resolution of airborne conflicts using Satisfiability Modulo Theories (SMT) solvers. Our approach takes a flight plan for an ownship, a set of immutable flight plans for traffic aircraft, and a set of constraints, and then returns a flight plan for the ownship that satisfies all constraints and is also conflict free with respect to the traffic aircraft. The constraints can relate to operational, business, or other aspects which must be considered while setting up the conflict resolution task as a constraint satisfaction problem. We present simulations of our approach using a prototype implementation based on \(\textsf {dReal}\), an SMT solver that is specialized for solving non-linear real function problems, showing promising results.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 89.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 64.99
Price includes VAT (United Kingdom)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Other SMT solvers, such as Z3 [7], which support non-linear arithmetic, do not fully support trigonometric functions, which is needed for this work.

  2. 2.

    We use the definition of [31] where \(\bar{F_o}\) has the same spatial configuration as \({F_o}\).

  3. 3.

    This problem statement aligns well with the discovery and synchronization service (DSS) based concept of operation for UAM where a provider of services for UAM (PSU) has to prove awareness of other PSUs with active operations in an area for its proposed operation to be accepted by the DSS of that area [6].

  4. 4.

    These constraints can also take into account factors like the aerodynamic capabilities of the ownship (e.g., fixed wing vs rotorcraft, flight-surface damage, etc.).

  5. 5.

    In this paper, the solution space is finite and bounded by a set of discrete ground speeds allowed for the ownship (see Sect. 2.1).

  6. 6.

    Depending on the use case, the constraints can be adjusted accordingly.

  7. 7.

    For simplicity, in this paper we assume the absence of wind. However, more complicated constraints may be designed by factoring in wind.

References

  1. Alejo, D., Cobano, J.A., Heredia, G., Ollero, A.: Collision-free 4D trajectory planning in unmanned aerial vehicles for assembly and structure construction. J. Intell. Robot. Syst. 73(1), 783–795 (2014)

    Article  Google Scholar 

  2. Ayhan, S., Costas, P., Samet, H.: Prescriptive analytics system for long-range aircraft conflict detection and resolution. In: Proceedings of the 26th ACM SIGSPATIAL International Conference on Advances in Geographic Information Systems, pp. 239–248 (2018)

    Google Scholar 

  3. Balachandran, S., Manderino, C., Muñoz, C., Consiglio, M.: A decentralized framework to support UAS merging and spacing operations in urban canyons. In: 2020 International Conference on Unmanned Aircraft Systems (ICUAS), pp. 204–210. IEEE (2020)

    Google Scholar 

  4. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15

    Chapter  Google Scholar 

  5. Colbert, B.K., Slagel, J.T., Crespo, L.G., Balachandran, S., Munoz, C.: Polysafe: a formally verified algorithm for conflict detection on a polynomial airspace. IFAC-PapersOnLine 53(2), 15615–15620 (2020)

    Article  Google Scholar 

  6. Craven, N., et al.: Report: X3 Simulation with National Campaign-Developmental Test (NC-DT) Airspace Partners. Technical report, National Aeronatics and Space Administration (2021). https://aviationsystems.arc.nasa.gov/publications/2021/NASA-TM-20210011098.pdf. Accessed 25 June 2021

  7. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  8. Dowek, G., Munoz, C., Carreño, V.: Provably safe coordinated strategy for distributed conflict resolution. In: AIAA Guidance, Navigation, and Control Conference and Exhibit, p. 6047 (2005)

    Google Scholar 

  9. Dowek, G., Munoz, C., Geser, A.: Tactical conflict detection and resolution in a 3-d airspace. Technical report INSTITUTE FOR COMPUTER APPLICATIONS IN SCIENCE AND ENGINEERING HAMPTON VA (2001)

    Google Scholar 

  10. Durand, N., Alliot, J.M., Noailles, J.: Automatic aircraft conflict resolution using genetic algorithms. In: Proceedings of the 1996 ACM Symposium on Applied Computing, pp. 289–298 (1996)

    Google Scholar 

  11. Ekici, B., et al.: SMTCoq: a plug-in for integrating SMT solvers into Coq. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 126–133. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_7

    Chapter  Google Scholar 

  12. 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., de Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol. 4576, pp. 177–188. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73445-1_13

    Chapter  Google Scholar 

  13. Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208–214. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_14

    Chapter  Google Scholar 

  14. Irfan, A., et al.: Towards verification of neural networks for small unmanned aircraft collision avoidance. In: 2020 AIAA/IEEE 39th Digital Avionics Systems Conference (DASC), pp. 1–10. IEEE (2020)

    Google Scholar 

  15. Katz, G., Barrett, C., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL (T)-based SMT solvers. In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp. 93–100. IEEE (2016)

    Google Scholar 

  16. Krozel, J., Peters, M., Bilimoria, K.D., Lee, C., Mitchell, J.S.: System performance characteristics of centralized and decentralized air traffic separation strategies. Air Traffic Control Q. 9(4), 311–332 (2001)

    Article  Google Scholar 

  17. Li, M., et al.: Requirements-based automated test generation for safety critical software. In: 2019 IEEE/AIAA 38th Digital Avionics Systems Conference (DASC), pp. 1–10. IEEE (2019)

    Google Scholar 

  18. Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646–662. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_43

    Chapter  Google Scholar 

  19. Meng, B., et al.: Towards a correct-by-construction design of integrated modular avionics. In: Conference on Formal Methods in Computer-Aided Design – FMCAD, p. 221 (2023)

    Google Scholar 

  20. Meng, B., et al.: Verdict: a language and framework for engineering cyber resilient and safe system. Systems 9(1), 18 (2021)

    Article  Google Scholar 

  21. Meng, B., Reynolds, A., Tinelli, C., Barrett, C.: Relational constraint solving in SMT. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 148–165. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_10

    Chapter  Google Scholar 

  22. Meng, B., Viswanathan, A., Smith, W., Moitra, A., Siu, K., Durling, M.: Synthesis of optimal defenses for system architecture design model in MaXSMT. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, vol. 13260, pp. 752–770. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-06773-0_40

    Chapter  Google Scholar 

  23. Munoz, C., Narkawicz, A., Chamberlain, J.: A TCAS-ii resolution advisory detection algorithm. In: AIAA Guidance, Navigation, and Control (GNC) Conference, p. 4622 (2013)

    Google Scholar 

  24. Murrieta-Mendoza, A., Botez, R.M., Patrón, R.S.F.: Flight altitude optimization using genetic algorithms considering climb and descent costs in cruise with flight plan information. Technical report SAE Technical Paper (2015)

    Google Scholar 

  25. Narkawicz, A., Muñoz, C., Dutle, A.: Sensor uncertainty mitigation and dynamic well clear volumes in DAIDALUS. In: 2018 IEEE/AIAA 37th Digital Avionics Systems Conference (DASC), pp. 1–8. IEEE (2018)

    Google Scholar 

  26. National Aeronatics and Space Administration: Range and Fuel Consumption Activity. https://www.grc.nasa.gov/www/k-12/BGP/Devon/range_fuel_act.htm. Accessed 18 June 2021

  27. Paul, S.: Emergency Trajectory Generation for Fixed-Wing Aircraft. Master’s thesis, Rensselaer Polytechnic Institute (2018)

    Google Scholar 

  28. Paul, S., Agha, G.A., Patterson, S., Varela, C.A.: Verification of eventual consensus in synod using a failure-aware actor model. In: Dutle, A., Moscato, M.M., Titolo, L., Muñoz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 249–267. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-76384-8_16

    Chapter  Google Scholar 

  29. Paul, S., et al.: Formal verification of safety-critical aerospace systems. IEEE Aerosp. Electron. Syst. Mag. 38(5), 72–88 (2023). https://doi.org/10.1109/MAES.2023.3238378

    Article  Google Scholar 

  30. Paul, S., Hole, F., Zytek, A., Varela, C.A.: Wind-aware trajectory planning for fixed-wing aircraft in loss of thrust emergencies. In: 2018 IEEE/AIAA 37th Digital Avionics Systems Conference (DASC), pp. 1–10 (2018).https://doi.org/10.1109/DASC.2018.8569842

  31. Paul, S., Patterson, S., Varela, C.A.: Conflict-aware flight planning for avoiding near mid-air collisions. In: The 38th AIAA/IEEE Digital Avionics Systems Conference (DASC 2019). San Diego, CA (2019).https://doi.org/10.1109/DASC43569.2019.9081658

  32. Peters, A., Balachandran, S., Duffy, B., Smalling, K., Consiglio, M., Muñoz, C.: Flight test results of a distributed merging algorithm for autonomous UAS operations. In: 2020 AIAA/IEEE 39th Digital Avionics Systems Conference (DASC), pp. 1–7. IEEE (2020)

    Google Scholar 

  33. Pritchett, A.R., Genton, A.: Negotiated decentralized aircraft conflict resolution. IEEE Trans. Intell. Transp. Syst. 19(1), 81–91 (2017)

    Article  Google Scholar 

  34. Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 244–261. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_16

    Chapter  Google Scholar 

  35. Sacharny, D., Henderson, T.C.: A lane-based approach for large-scale strategic conflict management for UAS service suppliers. In: 2019 International Conference on Unmanned Aircraft Systems (ICUAS), pp. 937–945. IEEE (2019)

    Google Scholar 

  36. Shone, R., Glazebrook, K., Zografos, K.G.: Applications of stochastic modeling in air traffic management: methods, challenges and opportunities for solving air traffic problems under uncertainty. Eur. J. Oper. Res. (2020)

    Google Scholar 

  37. Siu, K., et al.: Architectural and behavioral analysis for cyber security. In: 2019 IEEE/AIAA 38th Digital Avionics Systems Conference (DASC), pp. 1–10. IEEE (2019)

    Google Scholar 

  38. Yang, Y., Zhang, J., Cai, K.Q., Prandini, M.: Multi-aircraft conflict detection and resolution based on probabilistic reach sets. IEEE Trans. Control Syst. Technol. 25(1), 309–316 (2016)

    Article  Google Scholar 

  39. Young-Brown, F.: FUEL BURN RATES FOR PRIVATE AIRCRAFT (2015). https://www.sherpareport.com/aircraft/fuel-burn-private-aircraft.html. Accessed 18 June 2021

  40. Zhang, Y.J., Malikopoulos, A.A., Cassandras, C.G.: Optimal control and coordination of connected and automated vehicles at urban traffic intersections. In: 2016 American Control Conference (ACC), pp. 6227–6232. IEEE (2016)

    Google Scholar 

Download references

Acknowledgement

The authors would like to thank GE Aerospace Research for supporting the work and the reviewers of NFM 2024 for their detailed and constructive comments that helped improve the final manuscript.

Author information

Authors and Affiliations

  1. GE Aerospace Research, Niskayuna, NY, 12309, USA

    Saswata Paul, Baoluo Meng & Christopher Alexander

Authors
  1. Saswata Paul
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Baoluo Meng
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christopher Alexander
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Baoluo Meng .

Editor information

Editors and Affiliations

  1. NASA Ames Research Center, Moffett Field, CA, USA

    Nathaniel Benz

  2. Ames Research Center, Moffett Field, CA, USA

    Divya Gopinath

  3. NASA Ames Research Center, Moffet Field, CA, USA

    Nija Shi

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Paul, S., Meng, B., Alexander, C. (2024). SMT-Based Aircraft Conflict Detection and Resolution. In: Benz, N., Gopinath, D., Shi, N. (eds) NASA Formal Methods. NFM 2024. Lecture Notes in Computer Science, vol 14627. Springer, Cham. https://doi.org/10.1007/978-3-031-60698-4_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-60698-4_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-60697-7

  • Online ISBN: 978-3-031-60698-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation