CAREER: Designing Robust Cyber-Physical Systems: Logics, Automata, Optimization, and Heuristic Methods

该项目的影响是更可靠，更安全，性能更好的下一代网络物理系统（CPS）的工程设计，涉及汽车，医疗设备，航空电子，电网和自主代理。由于这些系统在无法完全预期/建模的环境中运行，因此从设计阶段开始就将鲁棒性作为主要目标至关重要。该项目的新奇是可扩展的和严格的正式算法的方法，以促进这种强大的CPS工程的发展。这些方法推进了经典的离散算法技术，用于CPS运行的定量环境中。该项目的研究方面与研究生和本科生课程的创建相辅相成，这些课程向即将进入劳动力市场的科学家和工程师教授核心逻辑和算法分析技能。CPS算法分析的第一步是系统预期正确行为的正式规范。信号时序逻辑（STL）是度量时序逻辑的信号变体，是目前流行的用于区分好/坏CPS行为的形式主义。不幸的是，STL不能指定工程师感兴趣的许多属性。该项目正在用其他时态操作符（如冻结操作符）来增强STL，以便具有更具表达力的规范形式，解决STL的缺点。这种增强是由高效算法、启发式方法和工具的开发指导的，并与之同步进行，以便新的逻辑易于在工业CPS环境中使用，例如，在测试生成中。正在探索增加规范表达性和由此增加的算法复杂性之间的权衡，以找到新CPS逻辑的易处理类。同样重要的是项目的推力，建立了一个理论的定量鲁棒性，这些新的形式主义，在空间和时间域。研究团队通过同行评审的会议和期刊出版物、会议演讲以及研究访问广泛传播研究成果。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The project's impact is the engineering of more reliable, safer, and better performing next generation Cyber-Physical Systems (CPS) arising in domains involving automotive vehicles, medical devices, avionics, power grids, and autonomous agents. As these systems operate in environments that cannot always be perfectly anticipated/modeled, it is crucial that robustness be a prime objective right from the design phase. The project's novelty is the development of scalable and rigorous formal algorithmic approaches for facilitating such robust CPS engineering. These approaches advance classical discrete algorithmic techniques for use in quantitative environments in which CPS operates. The research aspect of the project is complemented with the creation of graduate and undergraduate courses teaching core logical and algorithmic analyses skills to scientists and engineers about to enter the workforce.The first step toward algorithmic analysis of CPS is a formal specification of the expected correct behaviors of the system. Signal Temporal Logic (STL), the signal variant of Metric Temporal Logic, is currently a popular formalism for classifying good/bad CPS behaviors. Unfortunately, STL cannot specify many properties of interest to engineers. The project is augmenting STL with other temporal operators, such as the freeze operator, in order to have more expressive specification formalisms, addressing the shortcomings of STL. This augmentation is guided by, and done in tandem with, the development of efficient algorithms, heuristic methods, and tools so that the new logics will be tractable to use in industrial CPS contexts, for instance, in test generation. The tradeoff between increased specification expressivity and resulting increased algorithm complexity is being explored to find tractable classes of new CPS logics. Of equal importance is the project thrust that builds a theory of quantitative robustness over these new formalisms, both in the space and in the time domain. Broad dissemination of results is being done by the research team through peer reviewed conference and journal publications, conference talks, and through research visits.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.