Automated Construction of Dependable Component-based Cyber-physical Models

网络物理系统(CPS)是计算资源和物理资源紧密结合的系统。这种系统的例子包括自动防撞系统、医疗设备、自动搜索和救援设备以及航空电子系统。预计在不久的将来，这些系统的作用将大大扩大。为了实现这一潜力，未来的CPSS将需要是正确的，并显著提高效率和可靠性。这些目标带来了许多挑战。例如，我们目前缺乏形式化的方法来说明和推理CPSS的正确性。此外，还不清楚CPS环境中的约束如何影响被广泛理解的概念，如正确性、容错、维护和关注点分离。 在这个提案中，我主张开发基于模型的方法，这些方法可以自动构建通过构建正确的CPSS。基于模型的应用程序开发旨在通过使用在明确定义的转换步骤中使用的模型来提高完整性，从而产生按构造更正的构件。特别是，我认为CPSS本质上是基于组件的，因为物理和计算过程通常是相互通信的独立实体。因此，本研究计划将重点放在基于模型的容错组件型CPSS的开发上。具体地说，该项目的结果将是(1)用于基于组件的CPSS的形式化建模的简单、直观但具有表现力的框架，(2)用于向基于CPS的容错的基于组件的模型添加容错的自动形式化方法的严格的复杂性分析，(3)将容错与功能关注分离的转换方法和用于合成CPSS的充分条件，以及(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.