Formal Modelling is often used as part of the design and testing process of software development to ensure that components operate within suitable bounds even in unexpected circumstances. In this paper, we use predictive formal modelling (PFM) at runtime in a human-swarm mission and show that this integration can be used to improve the performance of human-swarm teams. We recruited 60 participants to operate a simulated aerial swarm to deliver parcels to target locations. In the PFM condition, operators were informed of the estimated completion times given the number of drones deployed, whereas in the No-PFM condition, operators did not have this information. The operators could control the mission by adding or removing drones from the mission and thereby, increasing or decreasing the overall mission cost. The evaluation of human-swarm performance relied on four key metrics: the time taken to complete tasks, the number of agents involved, the total number of tasks accomplished, and the overall cost associated with the human-swarm task. Our results show that PFM modelling at runtime improves mission performance without significantly affecting the operator's workload or the system's usability.

翻译：形式化建模常作为软件开发设计与测试过程的一部分，用于确保组件即使在意外情况下也能在适当范围内运行。本文在人类-无人机群任务中采用运行时预测形式化建模（PFM），并证明这种集成方法可提升人机群团队的绩效。我们招募了60名参与者操作模拟空中无人机群，将包裹运送至目标地点。在PFM条件下，操作员获知基于部署无人机数量的预估完成时间，而在非PFM条件下，操作员无此信息。操作员可通过增减任务中的无人机数量来控制任务进程，从而增加或降低总体任务成本。人机群绩效评估基于四个关键指标：任务完成时间、涉及智能体数量、完成总任务数及人机群任务相关总成本。研究结果表明，运行时PFM建模可在不显著影响操作员负荷或系统可用性的前提下，提升任务执行绩效。