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.