CPS: Small: Compositionality and Reconfiguration for Distributed Hybrid Systems

CPS：小号：分布式混合控制系统的组合性和可重构性本研究的目的是解决可重构分布式混合控制系统的验证和分析中的基本挑战。当连续工厂的控制决策取决于其他参与者的行为和状态时，这些情况经常发生。今天的核查技术并不支持这些措施。这里提倡的方法是开发严格的基于组合证明的验证技术，以缩小网络物理系统设计中的分析差距，并克服可扩展性问题。本项目开发使用微分方程的符号不变量的技术，以解决非线性应用和线性动力学的当前验证技术之间的分析差距。本项目旨在改变可以分析的系统范围的变革性研究。提出的研究开发了一种基于组合证明的混合系统验证方法，与主流的基于自动机的验证方法形成对比。它代表了一个重大的改进，解决了系统模型中的组合，重新配置和非线性的挑战。所提出的研究在下一代网络物理系统的安全关键属性的验证中具有重要的应用。这包括分布式汽车控制、机器人群和无人机合作计划，以实现多架飞机的完整防撞协议。分布式混合动力系统的分析工具具有广泛的应用范围，不同程度的安全关键性，验证成本和操作风险。发现漏洞或确保正确运行的分析技术可以挽救生命和金钱，因此可能产生重大的经济和社会影响。

CPS: Small: Compositionality and Reconfiguration for Distributed Hybrid SystemsThe objective of this research is to address fundamental challenges in the verification and analysis of reconfigurable distributed hybrid control systems. These occur frequently whenever control decisions for a continuous plant depend on the actions and state of other participants. They are not supported by verification technology today. The approach advocated here is to develop strictly compositional proof-based verification techniques to close this analytic gap in cyber-physical system design and to overcome scalability issues. This project develops techniques using symbolic invariants for differential equations to address the analytic gap between nonlinear applications and present verification techniques for linear dynamics.This project aims at transformative research changing the scope of systems that can be analyzed. The proposed research develops a compositional proof-based approach to hybrid systems verification in contrast to the dominant automata-based verification approaches. It represents a major improvement addressing the challenges of composition, reconfiguration, and nonlinearity in system models. The proposed research has significant applications in the verification of safety-critical properties in next generation cyber-physical systems. This includes distributed car control, robotic swarms, and unmanned aerial vehicle cooperation schemes to full collision avoidance protocols for multiple aircraft. Analysis tools for distributed hybrid systems have a broad range of applications of varying degrees of safety-criticality, validation cost, and operative risk. Analytic techniques that find bugs or ensure correct functioning can save lives and money, and therefore are likely to have substantial economic and societal impact.