This research seeks to lay down intellectual foundations for the static analysis of real-time control software as it interacts in closed-loop with physical systems. The approach taken is to cross-fertilize abstract interpretation and robust control system analysis. The goal is to combine the scalability of the former with the domain knowledge of the latter to support the development of static analyzers for embedded control software that can address systems containing several thousand lines of code. This cross-fertilization is facilitated by collaboration with one of the leading European teams working on abstract interpretation. The research is developing techniques for automatic generation of abstract models of control-related program semantics, using related abstract interpretation and robust control formalisms. The project also develops and adapts tools for validating the control-related program semantics, as they interact in closed-loop with the physical system. The work initially pursues the verification of simple properties, such as closed-loop system stability, continuing with more complex functional properties, such as reachability analyses to detect possible actuator saturation, and presence of limit cycles.
The project currently focuses primarily on aerospace applications; however it will impact any other applicative field where computers manage physical artifacts, such as power plants, automobiles and medical devices. The multi-disciplinary nature of the project is expected to lead to new perspectives on both formal analysis and control systems, enabling practitioners to analyze their systems not only at the specification level, but also the implementation level. This project also includes the development of a new educational curriculum aimed at bringing embedded software and control systems analysis together. This curriculum, which includes undergraduate and graduate components, aims at producing a new engineering workforce that is competent in both disciplines and knows how to use them jointly to facilitate future needs in embedded software system certification.
