CPS: Medium: Resource-Aware Hierarchical Runtime Verification for Mixed-Abstraction-Level Systems of Systems

驾驶飞机通常被描述为几个小时的极度无聊，其间不时出现可怕的恐惧。同样，前往遥远目标的航天器在很大程度上仍处于休眠状态，但需要定期增加维护和保持正常运行所需的活动。飞机和航天器是复杂的系统系统，必须无缝合作，通过精心编排的代表不同抽象级别的层次结构来切换控制，例如，事件的不同时间尺度就是例证。每个机载系统都面临着自己的验证挑战；面对潜在的意外环境输入，验证所有系统同时演奏的交响乐尤其令人望而生畏。我们可以用高效的运行时验证引擎来补充设计时验证，但它们需要增长到能够推理复杂系统系统的分层性质，其中单个需求可能需要封装多个抽象级别。最终结果必须能够在系统资源限制的范围内实时执行。现有的运行时验证工具不能遵守在真实系统(或真实任务)上运行它们所施加的约束，并且没有参数来将其计算需求集中在对系统安全影响最大的任务上。实现安全的CPS有赖于发展实时验证的工具和算法，将现实的安全检查融入到其控制体系结构和动态环境中，该项目采用形式化方法、控制理论、软硬件集成和软件工程等技术来设计运行时监视器，在不干扰系统正常运行的情况下对系统的网络物理系统进行检查。该项目设计、分析和实现了三个基本的运行时验证技术：规范中的混合抽象级粒度；资源感知以确保运行时监控器的非侵入性；以及使用模型预测来增强监控器以实现按时缓解触发。在为分层、混合抽象级别的规范建立新的形式语义，并在不干扰系统正常运行的情况下评估形式规范，同时在嵌入式CP的现实约束下最大化资源利用率方面，关键创新源于这一严密的基础。该项目将新理论概括为分层功能需求的规范模式，并合成预测模型，以实现更好、更自动地创建运行时验证配置，以满足现代CP的可扩展性需求。小型飞机群的飞行测试被用来验证这一方法。这一裁决反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Piloting an aircraft is popularly described as hours of abject boredom punctuated by periods of abject terror. Similarly, a spacecraft in transit to a distant target remains largely dormant but for periodic heightened activity required for maintenance and staying on course. Aircraft and spacecraft are complex systems of systems that must seamlessly work together, switching control through a carefully orchestrated hierarchy representing different levels of abstraction, e.g., exemplified by different timescales for events. Each on-board system presents its own verification challenge; verifying that the symphony of all of them playing together at the same time, in the face of potentially unexpected environmental inputs, is particularly daunting. We can supplement design-time verification with efficient runtime verification engines, but they need to grow to be able to reason about the hierarchical nature of complex systems-of-systems, where single requirements may need to encapsulate multiple levels of abstraction. The final result must be able to execute in real time, within system resource constraints. Existing tools for runtime verification aren't capable of obeying constraints imposed by running them on real systems (or in real missions), and don't have parameters to focus their computational demands on the tasks most impactful on system safety. Achieving safe CPS depends on growing the tools and algorithms of real-time verification to integrate realistic safety checks into their control architectures and dynamic environments.This project adapts techniques from formal methods, control theory, hardware-software integration, and software engineering to design runtime monitors that inspect cyber-physical systems of systems without interfering with their normal operation. The project designs, analyzes, and implements fundamental runtime verification techniques by dealing with three general and orthogonal problems: mixed-abstraction-level granularity in specifications, resource-awareness to ensure non-intrusiveness of runtime monitors, and augmenting monitors with model-prediction to enable on-deadline mitigation triggering. Key innovations stem from this rigorous foundation in establishing a new formal semantics for hierarchical, mixed-abstraction-level specification, and evaluating formal specifications without interfering with the system's normal operation, while maximizing utilization of resources within realistic constraints of embedded CPS. The project generalizes the new theory into specification patterns for hierarchical functional requirements and synthesize predictive models to enable better, more automated creation of runtime verification configurations to meet scalability demands of modern CPS. Flight tests of small aircraft swarms are used to validate this approach.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.