机构名称：
¥ 1.0
计算机科学的一个分支被称为“形式化方法”（FM），它专门使用数学逻辑形式对自动化系统的行为进行建模，这些逻辑可以使用机械化定理证明器和模型检查器进行非常强大的分析。有限状态机是 FM 中使用的形式化方法之一，该领域的研究人员最近开始将其方法应用于驾驶舱自动化。例如，Butler 等人 [2] 检查自动驾驶仪设计的一致行为，Leveson 等人 [11] 寻找被认为特别容易出错的构造，Rushby [15] 将自动驾驶仪描述与合理的心理模型进行比较。Leveson 和 Palmer [10] 以及 Rushby、Crow 和 Palmer [16] 展示了如何使用他们的方法预测 MD-88 自动驾驶仪 [12] 中已知的自动化意外。
整合人类的模型和机械化方法...
主要关键词
相关文件推荐
