Skip to main content

2017 | OriginalPaper | Buchkapitel

Reasoning About Safety-Critical Information Flow Between Pilot and Computer

verfasst von : Seth Ahrenbach

Erschienen in: NASA Formal Methods

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Literatur
1.
Zurück zum Zitat Ahrenbach, S., Goodloe, A.: Formal analysis of pilot error using agent safety logic. In: Innovations in Systems and Software Engineering (submitted) Ahrenbach, S., Goodloe, A.: Formal analysis of pilot error using agent safety logic. In: Innovations in Systems and Software Engineering (submitted)
2.
Zurück zum Zitat 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) 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)
3.
Zurück zum Zitat Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, New York (2001)CrossRefMATH Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, New York (2001)CrossRefMATH
4.
Zurück zum Zitat 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) 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)
5.
Zurück zum Zitat van Benthem, J.: Logical Dynamics of Information and Interaction. Cambridge University Press, New York (2011)CrossRefMATH van Benthem, J.: Logical Dynamics of Information and Interaction. Cambridge University Press, New York (2011)CrossRefMATH
7.
Zurück zum Zitat Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. The MIT Press, Cambridge (2003)MATH Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. The MIT Press, Cambridge (2003)MATH
8.
Zurück zum Zitat Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)MATH Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)MATH
9.
Zurück zum Zitat Hintikka, J.: Knowledge and Belief. Cornell University Press, Ithaca (1962)MATH Hintikka, J.: Knowledge and Belief. Cornell University Press, Ithaca (1962)MATH
10.
Zurück zum Zitat Klir, G., Yuan, B.: Fuzzy Sets and Fuzzy Logic, vol. 4. Prentice Hall, New Jersey (1995)MATH Klir, G., Yuan, B.: Fuzzy Sets and Fuzzy Logic, vol. 4. Prentice Hall, New Jersey (1995)MATH
11.
Zurück zum Zitat Lescanne, P.: Mechanizing common knowledge logic using COQ. Ann. Math. Artif. Intell. 48(1–2), 15–43 (2006). APAMathSciNetMATH Lescanne, P.: Mechanizing common knowledge logic using COQ. Ann. Math. Artif. Intell. 48(1–2), 15–43 (2006). APAMathSciNetMATH
12.
Zurück zum Zitat Maliković, M., Čubrilo, M.: Modeling epistemic actions in dynamic epistemic logic using Coq. In: CECIIS 2010 (2010) Maliković, M., Čubrilo, M.: Modeling epistemic actions in dynamic epistemic logic using Coq. In: CECIIS 2010 (2010)
13.
Zurück zum Zitat Maliković, M., Čubrilo, M.: Reasoning about epistemic actions and knowledge in multi-agent systems using Coq. Comput. Technol. Appl. 2(8), 616–627 (2011) Maliković, M., Čubrilo, M.: Reasoning about epistemic actions and knowledge in multi-agent systems using Coq. Comput. Technol. Appl. 2(8), 616–627 (2011)
14.
Zurück zum Zitat 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) 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)
Metadaten
Titel
Reasoning About Safety-Critical Information Flow Between Pilot and Computer
verfasst von
Seth Ahrenbach
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-57288-8_25

Premium Partner