CSR/EHS - Certification of Safety-Critical Control Software

Feron abstract本研究旨在为实时控制软件与物理系统在闭环中相互作用时的静态分析奠定智力基础。所采取的方法是将抽象解释和鲁棒控制系统分析相结合。目标是将前者的可伸缩性与后者的领域知识相结合，以支持嵌入式控制软件的静态分析器的开发，这些分析器可以处理包含数千行代码的系统。通过与一个致力于抽象解释的欧洲领先团队的合作，促进了这种交叉受精。利用相关的抽象解释和鲁棒控制形式，开发控制相关程序语义抽象模型的自动生成技术。该项目还开发和调整了用于验证与控制相关的程序语义的工具，因为它们与物理系统在闭环中相互作用。这项工作最初是为了验证简单的特性，如闭环系统的稳定性，然后继续进行更复杂的功能特性，如可达性分析，以检测可能的执行器饱和，以及极限环的存在。该项目目前主要侧重于航空航天应用；然而，它将影响计算机管理物理工件的任何其他应用领域，如发电厂、汽车和医疗设备。项目的多学科性质预计将导致对形式分析和控制系统的新观点，使从业者不仅能够在规范级别上分析他们的系统，而且能够在实现级别上分析他们的系统。该项目还包括开发新的教育课程，旨在将嵌入式软件和控制系统分析结合在一起。本课程包括本科生和研究生两部分，旨在培养一群在这两个学科都有能力的新工程师，并知道如何将它们结合起来，以促进嵌入式软件系统认证的未来需求。

Feron AbstractThis 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.