CPS: Synergy: Collaborative Research: Methodologies for Engineering with Plug-and-Learn Components: Formal Synthesis and Analysis Across Abstraction Layers

复杂设备的有效工程通常主要依赖于将任务职责封装到模块化代理中的能力，并确保这些代理以定义良好且易于观察的方式相互通信。当满足这些条件时，就有可能发现问题所在，从而纠正问题。还可以优化代理及其通信以提高性能。网络物理系统（如机器人，自动驾驶飞机等）修改自己以提高性能，打破了一些代理模块协商自己的通信并决定自己的行动的条件，有时以我们没有预料到的方式利用世界的物理特性。这使得难以应用标准的工程工具来完成关键故障诊断和设计优化。该项目将产生分析方法，以解决网络物理系统的特定需求，就其性质而言，打破惯例的规则。我们将这些新方法应用于扑翼微型飞行器自改进控制器的设计和分析。这项工作将在模型检查相关的正式设计方法和计算资源受限的网络物理系统中基于模块的自适应控制方面取得进展。形式化方法的进步将显著扩展我们正确设计和验证紧密耦合计算、传感器和执行器的系统的能力。具体的测试应用对许多国家重要的安全和国防工作具有重要意义，并将直接影响确定的国家优先事项。

Effective engineering of complex devices often depends critically on the ability to encapsulate responsibility for tasks into modular agents and ensure those agents communicate with one another in well-defined and easily observable ways. When such conditions are followed, it becomes possible to detect where problems lie so they can be corrected. It also becomes possible to optimize the agents and their communications to improve performance. Cyber-physical systems (like robots, self-piloting aircraft, etc.) modify themselves to improve performance break those conditions in that some agent modules negotiate their own communications and decide their own actions, sometimes taking advantage of the physics of the world in ways we did not anticipate. This renders difficult application of standard engineering tools to accomplish critical fault diagnosis and design optimization. This project will produce analysis methods address the specific needs of cyber-physical systems that, by their natures, break the rules of convention. We will apply these new methods to the design and analysis of self-improving controllers for flapping-wing micro air vehicles. This work will provide advances in both model-checking related formal design methodologies and in module-based self-adaptive control in computationally resource constrained cyber-physical systems. The formal methods advances will significantly expand our ability to properly design and verify systems that tightly couple computation, sensors, and actuators. The specific test application addressed is significant to a number of nationally important security and defense efforts and will directly impact identified national priorities.