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

Colorado State University, Fort Collins CO

Investigators

Abstract

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.