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.