Borzoo Bonakdarpour has been awarded a grant from the National Science Foundation

Abstract:

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.

We adapt 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. We will design, analyze, and implement 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 our 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. We generalize 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 will validate our approach.