关于飞行员与计算机之间安全关键信息流的推理
计算机科学中的逻辑
2018-12-27 v1
摘要
本文展示了开发一种动态逻辑的研究成果，用于推理人类与计算机之间安全关键的信息流。该逻辑推进了先前开发智能体知识逻辑的努力，后者对现实中的人类智能体做出了过强的假设。我们引入了动态智能体安全逻辑(DASL)，它基于动态认知逻辑(DEL)，并进行了扩展以考虑安全动作、信念，以及知识、信念与安全动作之间的逻辑关系。利用该逻辑，我们可以推断出飞行员在执行不安全动作时缺失了哪些安全关键信息。我们将该逻辑应用于法国航空447号航班事故作为案例研究，并在 Coq 证明助手中提供了该案例的机械化证明。
引用
@article{arxiv.1812.10363,
title = {Reasoning About Safety-Critical Information Flow Between Pilot and Computer},
author = {Seth Ahrenbach},
journal= {arXiv preprint arXiv:1812.10363},
year = {2018}
}
备注
Published in the Proceedings from the 9th International Symposium of NASA Formal Methods, 2017