CPS: Breakthrough: Scalable Component-Based Model Revision of Cyber-Physical Systems with Separation of Concerns

该项目开发了用于修改网络物理系统给定模型的算法，同时确保修改后的模型是正确的，并且可以在网络物理系统施加的约束中实现。它将这些算法专门用于容错（使用关注点分离理论）和时间模型（使用公平性角色）的上下文中。项目识别由于无法修改部分或全部物理组件而施加的约束，并确保在修订期间满足它们。它专门研究了两种情况下的模型修正算法：容错和修正过程中的公平作用。在容错方面，提出了网络物理系统的关注点分离理论。这项工作弥补了容错组件、控制理论和模型修正之间的差距。在公平性方面，利用抽象对连续行为和利用公平性的离散行为进行建模，开发了有效的修正算法。该项目的一个广泛影响是通过开发系统方法来推进网络物理系统的基础科学和技术，确保系统在因需求和/或环境变化而修改的维护期间的正确性。该项目的算法将为汽车和航空系统提供保证技术。在添加了容错属性的上下文中，所建议的活动也有可能及早识别缺失的规范，从而降低设计相应系统的成本。建议的活动有助于教育研究生关于通过基于组件的模型和通过模型修订提供保证所涉及的不同任务。

This project develops algorithms for revising a given model for a cyber-physical system while ensuring that the revised model is correct-by-construction and is realizable in the constraints imposed by the cyber-physical system. It specializes these algorithms in the context of fault-tolerance (with the theory of separation of concerns) and in the context of timed models (with the role of fairness). The project identifies constraints imposed by the inability to revise some or all physical components and ensure that they are satisfied during revision. It specializes model revision algorithms in two contexts: fault-tolerance and role of fairness during revision. Regarding fault-tolerance, it develops the theory of separation of concerns for cyber-physical systems. This work bridges the gap between fault-tolerance components, control theory and model revision. Regarding fairness, it develops efficient algorithms for revision by using abstraction to model continuous behaviors with discrete behaviors that utilize fairness. One broad impact of this project is to advance the fundamental science and technology of cyber-physical systems by developing systematic methods that ensure system correctness during maintenance where the system is revised due to changing requirements and/or environment. The algorithms from this project will provide techniques for providing assurance in automotive and aeronautical systems. In the context where fault-tolerance properties are added, the proposed activities also have the potential to identify missing specifications early and thereby reduce the cost of designing corresponding systems. The proposed activities facilitate in educating graduate students about different tasks involved in providing assurance via component based models and via model revision.