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.