CPS: Medium: Safety-Critical Wireless Mobile Systems

自主移动的系统的时代正在到来--从自主汽车到家用机器人再到空中无人机--它们有望改变多个行业，并对美国经济产生重大影响。通过无线协调，这些系统创造了一个大于其部分之和的整体。例如，车辆“排”通过几乎保险杠到保险杠的行驶，使用无线耦合同时制动和加速，从而增加了高速公路的吞吐量和燃油效率。类似地，车辆或无人机可以利用前面智能体的感知能力在盲角附近加速。然而，无线通信仍然被认为对于像这样的安全关键操作太不可靠。这项研究正在为安全的无线协调移动性创造新的技术，随着自主移动的系统的扩散，这种技术变得越来越重要。该方法是开发一个框架，联合建模和分析的运动和通信，以找到可证明安全的协调路径。这包括可以预测运动路径对无线信道的影响的新模型，以及可以以易于处理的方式使用这些模型来合成具有可证明保证的控制策略的新形式化方法。关键的创新包括评估射频模型有效性的新方法，在无线信道和协议的复杂模型上进行易处理的概率推理的新方法，以及为没有无线协调就不安全的状态实现可证明的安全保证的新控制策略。如果成功，这项研究将使移动的系统实现无线协调的性能优势，同时保持提供可证明的安全保证的能力。重点不是提高无线信道的可靠性，而是通过对信道在快速变化环境中的动态特性进行建模和分析，为整个移动的系统提供安全保障。

The age of autonomous mobile systems is dawning -- from autonomous cars to household robots to aerial drones -- and they are expected to transform multiple industries and have significant impact on the US economy. Through wireless coordination, these systems create a whole that is greater than the sum of its parts. For example, vehicle "platoons" increase both highway throughput and fuel efficiency by traveling nearly bumper-to-bumper, using a wireless coupling to brake and accelerate simultaneously. Similarly, vehicles or drones can speed around blind corners using the sensing capabilities of the agents ahead of them. However, wireless communication is still considered too unreliable for safety-critical operations like these. This research is creating new techniques for safe wirelessly coordinated mobility, which is becoming increasingly important with the proliferation of autonomous mobile systems. The approach is to develop a framework for joint modeling and analysis of motion and communication in order to find provably safe coordination paths. This includes new models that can predict the effect of motion paths on the wireless channel, together with new formal methods that can use these models in a tractable manner to synthesize control strategies with provable guarantees. The key innovations include new methods to assess the validity of a Radio Frequency model, new methods for tractable probabilistic reasoning over complex models of the wireless channel and protocols, and new control strategies that achieve provable safety guarantees for states that would have been unsafe without wireless coordination. If successful, this research will allow mobile systems to realize the performance benefits of wireless coordination while preserving the ability to provide provable safety guarantees. The focus is not on improving the wireless channel reliability; instead, the aim is to provide safety guarantees on the entire mobile system by modeling and analyzing the channel's dynamic properties in a rapidly changing environment.