Skip to main content
SpringerLink
Log in

Probabilistic Formal Verification of the SATS Concept of Operation

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

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9690))

Included in the following conference series:

Abstract

The objective of NASA’s Small Aircraft Transportation System (SATS) Concept of Operations (ConOps) is to facilitate High Volume Operation (HVO) of advanced small aircraft operating in non-towered non-radar airports. Given the safety-critical nature of SATS, its analysis accuracy is extremely important. However, the commonly used analysis techniques, like simulation and traditional model checking, do not ascertain a complete verification of SATS due to the wide range of possibilities involved in SATS or the inability to capture the randomized and unpredictable aspects of the SATS ConOps environment in their models. To overcome these limitations, we propose to formulate the SATS ConOps as a fully synchronous and probabilistic model, i.e., SATS-SMA, that supports simultaneously moving aircraft. The distinguishing features of our work include the preservation of safety of aircraft while improving throughput at the airport. Important insights related to take-off and landing operations during the Instrument Meteorological Conditions (IMC) are also presented.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • 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

References

  1. Instrument Procedures Handbook. U.S. Department of Transportation, Federal Aviation Administration (2015)

    Google Scholar 

  2. PRISM - Probabilistic Symbolic Model Checker (2016). http://www.prismmodelchecker.org

  3. Arons, T., Pnueli, A., Ruah, S., Xu, Y., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221–234. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Bai, C., Zhang, X.: Aircraft landing scheduling in the small aircraft transportation system. In: International Conference on Computational and Information Sciences, pp. 1019–1022. IEEE (2011)

    Google Scholar 

  5. Baier, C., Katoen, J.P., et al.: Principles of model checking, vol. 26202649. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  6. Baxley, B., Williams, D., Consiglio, M., Adams, C., Abbott, T.: The small aircraft transportation system (SATS), higher volume operations (HVO) off-nominal operations. In: Aviation, Technology, Integration, and Operations Conference. American Institute of Aeronautics and Astronautics (2005)

    Google Scholar 

  7. Baxley, B., Williams, D., Consiglio, M., Adams, C., Abbott, T.: Small aircraft transportation system, higher volume operations concept and research summary. J. Aircr. 45(6), 1825–1834 (2008)

    Article  Google Scholar 

  8. Carreño, V.: Concept for multiple operations at non-tower non-radar airports during instrument meteorological conditions. In: Digital Avionics Systems Conference, vol. 1, pp. 5.B.1–5.1-9. IEEE (2003)

    Google Scholar 

  9. Carreño, V., Muñoz, C.: Safety verification of the small aircraft transportation system concept of operations. In: Aviation, Technology, Integration, and Operations Conference. American Institute of Aeronautics and Astronautics (2005)

    Google Scholar 

  10. Cheng, A., Niktab, H., Walston, M.: Timing analysis of small aircraft transportation system (SATS). In: Conference on Embedded and Real-Time Computing Systems and Applications, pp. 58–67. IEEE (2012)

    Google Scholar 

  11. Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  12. Consiglio, M., Conway, S., Adams, C., Syed, H.: SATS HVO procedures for priority landings and mixed VFR/IFR operations. In: Digital Avionics Systems Conference, vol. 2, pp. 13.B.2-1–13.B.2-8. IEEE (2005)

    Google Scholar 

  13. Dowek, G., Munoz, C., Carreño, V.A.: Abstract model of the SATS concept of operations: Initial results and recommendations. Technical report NASA/TM-2004-213006, NASA Langley Research Center (2004)

    Google Scholar 

  14. Fedeli, A., Fummi, F., Pravadelli, G.: Properties incompleteness evaluation by functional verification. IEEE Trans. Comput. 56(4), 528–544 (2007)

    Article  MathSciNet  Google Scholar 

  15. Gariel, M., Spieser, K., Frazzoli, E.: On the statistics and predictability of go-arounds. In: Conference on Intelligent Data Understanding (2011)

    Google Scholar 

  16. Greco, A., Magyarits, S., Doucett, S.: Air traffic control studies of small aircraft transportation system operations. In: Digital Avionics Systems Conference, vol. 2, pp. 13.A.4-1–13.A.4-12. IEEE (2005)

    Google Scholar 

  17. Güdemann, M., Ortmeier, F.: A framework for qualitative and quantitative formal model-based safety analysis. In: Symposium on High-Assurance Systems Engineering, pp. 132–141. IEEE (2010)

    Google Scholar 

  18. Hoque, K.A., Mohamed, O.A., Savaria, Y.: Towards an accurate reliability, availability and maintainability analysis approach for satellite systems based on probabilistic model checking. In: Design, Automation Test in Europe Conference Exhibition, pp. 1635–1640. IEEE (2015)

    Google Scholar 

  19. Johnson, T.T., Mitra, S.: Parameterized verification of distributed cyber-physical systems: an aircraft landing protocol case study. In: International Conference on Cyber-Physical Systems, pp. 161–170. IEEE (2012)

    Google Scholar 

  20. Johnson, T.T., Mitra, S.: A small model theorem for rectangular hybrid automata networks. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 18–34. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  21. Johnson, T.T., Mitra, S.: Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems. In: Infotech at Aerospace Conference. American Institute of Aeronautics and Astronautics (2013)

    Google Scholar 

  22. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  23. Muñoz, C., Dowek, G., Carreño, V.: Modeling and verification of an air traffic concept of operations. Softw. Eng. Notes 29(4), 175–182 (2004)

    Article  Google Scholar 

  24. Muñoz, C., Carreño, V.A., Dowek, G.: Formal analysis of the operational concept for the small aircraft transportation system. In: Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.) Rigorous Development of Complex Fault-Tolerant Systems. LNCS, vol. 4157, pp. 306–325. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  25. Muñoz, C., Dowek, G.: Hybrid verification of an air traffic operational concept. In: IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation (2005)

    Google Scholar 

  26. Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)

    Google Scholar 

  27. Peters, M.: Capacity analysis of the NASA Langley airport management module. In: Digital Avionics Systems Conference, vol. 1, pp. 4.D.6–41–12. IEEE (2005)

    Google Scholar 

  28. Sardar, M.U., Hoque, K.A.: Probabilistic formal verification of the SATS concept of operation (2016). http://save.seecs.nust.edu.pk/projects/SATS

  29. Umeno, S., Lynch, N.A.: Proving safety properties of an aircraft landing protocol using I/O automata and the PVS theorem prover: a case study. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 64–80. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  30. Viken, S.A., Brooks, F.M.: Demonstration of four operating capabilities to enable a small aircraft transportation system. In: Digital Avionics Systems Conference, vol. 2, pp. 13.A.1-1–13.A.1-16. IEEE (2005)

    Google Scholar 

  31. Williams, D.M.: Point-to-point! validation of the small aircraft transportation system higher volume operations concept. In: International Congress of Aeronautical Sciences (2006)

    Google Scholar 

  32. Williams, D., Consiglio, M., Murdoch, J., Adams, C.: Flight technical error analysis of the SATS higher volume operations simulation and flight experiments. In: Digital Avionics Systems Conference, vol. 2, pp. 13.B.1-1–13.B.1-12. IEEE (2005)

    Google Scholar 

  33. Xu, Y., Baik, H., Trani, A.: A preliminary assessment of airport noise and emission impacts induced by small aircraft transportation system operations. In: Aviation Technology, Integration and Operations Conference. American Institute of Aeronautics and Astronautics (2006)

    Google Scholar 

Download references

Acknowledgments

We would like to express our profound gratitude and heartfelt thanks to Dr. Cesar A. Munoz from NASA Langley Research Center for the valuable insights related to SATS and their model. We are also enormously pleased to precise our intense gratefulness and deepest gratitude to Dr. Matthias Gudemann for his helpful tips on modeling the system in PRISM. K. A. Hoque and T. T. Johnson are supported in part by the National Science Foundation (NSF) via grant number CNS 1464311, the Air Force Research Laboratory (AFRL) via contract number FA8750-15-1-0105, and the Air Force Office of Scientific Research (AFOSR) via contract number FA9550-15-1-0258. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of AFRL, AFOSR, or NSF.

Author information

Authors and Affiliations

  1. School of Electrical Engineering and Computer Science (SEECS), National University of Sciences and Technology (NUST), Islamabad, Pakistan

    Muhammad Usama Sardar, Nida Afaq & Osman Hasan

  2. Department of Computer Science and Engineering (CSE), University of Texas at Arlington, Arlington, USA

    Khaza Anuarul Hoque & Taylor T. Johnson

Authors
  1. Muhammad Usama Sardar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nida Afaq
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Khaza Anuarul Hoque
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Taylor T. Johnson
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Osman Hasan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Muhammad Usama Sardar .

Editor information

Editors and Affiliations

  1. University of Minnesota, Minneapolis, Minnesota, USA

    Sanjai Rayadurgam

  2. NASA Ames Research Center , Moffett Field, California, USA

    Oksana Tkachuk

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Sardar, M.U., Afaq, N., Hoque, K.A., Johnson, T.T., Hasan, O. (2016). Probabilistic Formal Verification of the SATS Concept of Operation. In: Rayadurgam, S., Tkachuk, O. (eds) NASA Formal Methods. NFM 2016. Lecture Notes in Computer Science(), vol 9690. Springer, Cham. https://doi.org/10.1007/978-3-319-40648-0_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40648-0_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40647-3

  • Online ISBN: 978-3-319-40648-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation