On Using Composability Tools for Reliability Analysis of Unmanned Multi-Aircraft Systems: A Case Study
On Using Composability Tools for Reliability Analysis of Unmanned Multi-Aircraft Systems: A Case Study
复制标题
DOI：
10.1109/access.2020.2966763
复制
发表时间：
2020-01
期刊：
影响因子：
3.9
通讯作者：
D. Muniraj;Dany Abou Jaoude;M. Farhood
中科院分区：
文献类型：
--
作者：
D. Muniraj;Dany Abou Jaoude;M. Farhood
本文提出了一个案例研究，展示了如何使用组合验证工具来设计和分析在动态和不确定环境中运行的复杂多智能体系统。该案例研究涉及无人多机系统的设计，其任务是通过部署对抗措施来破坏空中入侵者。组成人员被称为防御者，是固定翼无人机。为了成功地危害入侵者，至少一名防御者必须在一定时间内与入侵者保持在预定距离内，并且防御者必须避免彼此之间以及与入侵者发生碰撞。由于组件（防御者）及其之间的交互的复杂性，使用整体（系统级）验证技术验证此全局属性是一项具有挑战性的任务。为了克服这些挑战，组件被设计为具有模块化架构，从而能够使用基于组件的推理来简化验证全局系统属性的任务。欧几里得几何和形式方法的结果用于证明大多数组件属性。对于分析工具过于保守的属性，进行集中的蒙特卡罗模拟。将模拟（或测试）的使用限制为局部组件属性的验证可以提高系统的可靠性。
This paper presents a case study that demonstrates how tools from compositional verification can be used to design and analyze complex multi-agent systems operating in dynamic and uncertain environments. The case study concerns the design of an unmanned multi-aircraft system tasked to compromise an aerial encroacher by deploying countermeasures. The constituent agents, termed defenders, are fixed-wing unmanned aircraft. To successfully compromise the encroacher, at least one defender must be within a prespecified distance from the encroacher for a certain period, and the defenders must avoid collision among themselves and with the encroacher. Verifying this global property using monolithic (system-level) verification techniques is a challenging task due to the complexity of the components (defenders) and the interactions among them. To overcome these challenges, the components are designed to have a modular architecture, thereby enabling the use of component-based reasoning to simplify the task of verifying the global system property. Results from Euclidean geometry and formal methods are used to prove most component properties. For properties where analytical tools are overly conservative, focused Monte Carlo simulations are carried out. Restricting the use of simulations (or testing) to local verification of partial component properties leads to increasing the reliability of the system.