Skip to main content
SpringerLink
Log in
Book cover

NASA Formal Methods Symposium

NFM 2017: NASA Formal Methods pp 342–356Cite as

Reasoning About Safety-Critical Information Flow Between Pilot and Computer

  • Conference paper
  • First Online:

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

Abstract

This paper presents research results that develop a dynamic logic for reasoning about safety-critical information flow among humans and computers. The logic advances previous efforts to develop logics of agent knowledge, which make assumptions that are too strong for realistic human agents. We introduce Dynamic Agent Safety Logic (DASL), based on Dynamic Epistemic Logic (DEL), with extensions to account for safe actions, belief, and the logical relationships among knowledge, belief, and safe action. With this logic we can infer which safety-critical information a pilot is missing when executing an unsafe action. We apply the logic to the Air France 447 incident as a case study and provide a mechanization of the case study in the Coq proof assistant.

This is a preview of subscription content, 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   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Notes

  1. 1.

    Code: https://github.com/sethkurtenbach/DASL/blob/master/DASL.v.

References

  1. Ahrenbach, S., Goodloe, A.: Formal analysis of pilot error using agent safety logic. In: Innovations in Systems and Software Engineering (submitted)

    Google Scholar 

  2. Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., Parent, C.: The Coq proof assistant reference manual: version 6.1 (Doctoral dissertation, Inria) (1997)

    Google Scholar 

  3. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, New York (2001)

    Book  MATH  Google Scholar 

  4. Bureau d’Enquêtes et d’Analyses: Final report on the accident on 1st June 2009 to the Airbus A330-203 registered F-GZCP operated by Air France flight AF 447 Rio de Janeiro-Paris. BEA, Paris (2012)

    Google Scholar 

  5. van Benthem, J.: Logical Dynamics of Information and Interaction. Cambridge University Press, New York (2011)

    Book  MATH  Google Scholar 

  6. Van Ditmarsch, H.: Knowledge games. Bull. Econ. Res. 53(4), 249–273 (2001)

    Article  MathSciNet  Google Scholar 

  7. Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. The MIT Press, Cambridge (2003)

    MATH  Google Scholar 

  8. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  9. Hintikka, J.: Knowledge and Belief. Cornell University Press, Ithaca (1962)

    MATH  Google Scholar 

  10. Klir, G., Yuan, B.: Fuzzy Sets and Fuzzy Logic, vol. 4. Prentice Hall, New Jersey (1995)

    MATH  Google Scholar 

  11. Lescanne, P.: Mechanizing common knowledge logic using COQ. Ann. Math. Artif. Intell. 48(1–2), 15–43 (2006). APA

    MathSciNet  MATH  Google Scholar 

  12. Maliković, M., Čubrilo, M.: Modeling epistemic actions in dynamic epistemic logic using Coq. In: CECIIS 2010 (2010)

    Google Scholar 

  13. Maliković, M., Čubrilo, M.: Reasoning about epistemic actions and knowledge in multi-agent systems using Coq. Comput. Technol. Appl. 2(8), 616–627 (2011)

    Google Scholar 

  14. National Transportation Safety Board: Descent below visual glidepath and impact with Seawall Asiana Flight 214, Boeing 777-200ER, HL 7742, San Francisco, California, 6 July 2013 (Aircraft Accident Report NTSB/AAR-14/01). NTSB, Washington, DC (2014)

    Google Scholar 

Download references

Acknowledgements

Seth Ahrenbach was partially supported by NSF CNS 1553548. The author is grateful for the criticism and suggestions provided by anonymous reviewers, and for the very generous assistance from Alwyn Goodloe, Rohit Chadha, and Chris Hathhorn.

Author information

Authors and Affiliations

  1. University of Missouri, Columbia, Missouri, 65201, USA

    Seth Ahrenbach

Authors
  1. Seth Ahrenbach
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Seth Ahrenbach .

Editor information

Editors and Affiliations

  1. Stanford University, Palo Alto, California, USA

    Clark Barrett

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

    Misty Davies

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

    Temesghen Kahsai

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Ahrenbach, S. (2017). Reasoning About Safety-Critical Information Flow Between Pilot and Computer. In: Barrett, C., Davies, M., Kahsai, T. (eds) NASA Formal Methods. NFM 2017. Lecture Notes in Computer Science(), vol 10227. Springer, Cham. https://doi.org/10.1007/978-3-319-57288-8_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-57288-8_25

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-57287-1

  • Online ISBN: 978-3-319-57288-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation