人机团队中渐趋自主系统的保障:城市空中交通案例研究
软件工程
2021-10-27 v1 人机交互
计算机科学中的逻辑
摘要
随着飞机系统日益自主化,人机角色分配发生变化,并出现了新的失效模式。这需要一种方法来识别渐趋自主系统(IAS)的安全需求,以及一套框架与技术来验证和确认 IAS 满足其安全需求。我们利用机组资源管理技术来识别安全人机协作行为的需求与行为。我们提供了一种验证 IAS 满足其需求的方法论。我们将该方法论应用于城市空中交通的案例研究,其中包含两种应急场景:传感器不可靠与着陆中止。在本案例研究中,我们用 Soar 语言实现了一个 IAS 智能体,作为所选应急场景的副驾驶,执行起飞与着陆准备,而飞行员保留最终决策权。我们在体系结构分析与设计语言(AADL)中建立了形式化人机团队体系结构模型,并将操作员与 IAS 需求在 AADL 的假设保证推理环境(AGREE)附件中形式化。给定对 IAS 和操作员的需求,我们形式化验证了人机团队的安全需求。我们开发了从 Soar 到 nuXmv 模型检测语言的自动翻译器,并使用 nuXmv 形式化验证 IAS 智能体满足其需求。我们分享了在此过程中发现的设计与需求错误以及所得经验教训。
引用
@article{arxiv.2110.12591,
title = {Assuring Increasingly Autonomous Systems in Human-Machine Teams: An Urban Air Mobility Case Study},
author = {Siddhartha Bhattacharyya and Jennifer Davis and Anubhav Gupta and Nandith Narayan and Michael Matessa},
journal= {arXiv preprint arXiv:2110.12591},
year = {2021}
}
备注
In Proceedings FMAS 2021, arXiv:2110.11527