Automated Construction of Dependable Component-based Cyber-physical Models

信息物理系统（CPS）是一个计算资源和物理资源紧密结合的系统。这种系统的示例包括自主防撞系统、医疗设备、自主搜索和救援设备以及航空电子系统。预计这些系统的作用将在不久的将来大大扩大。为了实现这一潜力，未来的CPS将需要是正确的，并且更加有效和可靠。这些目标带来了许多挑战。例如，我们目前缺乏正式的方法来指定和推理CPS的正确性。此外，目前还不清楚CPS环境中的约束如何影响广泛理解的概念，如正确性，容错，维护和分离的关注。 在这个建议中，我提倡开发基于模型的方法，自动构建通过构造而正确的CPS。基于模型的应用程序开发旨在通过使用在清晰定义的转换步骤中使用的模型来增加完整性，从而导致正确的构建工件。特别是，我认为CPS本质上是基于组件的，因为物理和计算过程通常是相互通信的独立实体。因此，本研究计划将侧重于基于模型的容错组件的CPS的开发。具体来说，这个项目的成果将是（1）一个简单，直观，但表达框架的形式化建模的组件为基础的CPS，（2）严格的复杂性分析的自动化形式化方法添加容错到一个容错组件为基础的模型的CPS，（3）转换方法，分离容错功能的关注和充分条件的CPS合成，（4）在实践中实现理论成果的有力工具链。

A cyber-physical system (CPS) is a system in which there is a tight conjoining between computational and physical resources. Examples of such a system include autonomous collision avoidance systems, medical devices, autonomous search and rescue devices, and avionics systems. It is expected that the role of these systems will expand significantly in the near future. To realize this potential, future CPSs will need to be correct and significantly more efficient and dependable. These objectives introduce numerous challenges. For example, we currently lack formal methods for specifying and reasoning about the correctness of CPSs. Moreover, it is unclear how constraints in a CPS's environment affect widely understood notions such as correctness, fault-tolerance, maintenance, and separation of concerns. In this proposal, I advocate the approach of developing model-based methods that automatically build CPSs that are correct by construction. Model-based application development aims at increasing the integrity by using models employed in clearly defined transformation steps leading to correct-by-construction artifacts. In particular, I would argue that CPSs are inherently component-based, as physical and computational processes are normally stand-alone entities communicating with each other. Thus, this research program will focus on model-based development of fault-tolerant component-based CPSs. Specifically, the outcome of this project will be (1) a simple, intuitive, and yet expressive framework for formal modeling of component-based CPSs, (2) rigorous complexity analysis of automated formal methods for adding fault-tolerance to a fault-intolerant component-based model of a CPS, (3) transformation methods that separate fault-tolerance from functional concerns and sufficient conditions for compositional synthesis of CPSs, and (4) a powerful tool chain that realizes the theoretical results in practice.