Algorithmic Synthesis of Embedded Controllers

嵌入式控制器的算法综合近年来，微处理器已经侵入了物理世界，导致了复杂而复杂的网络嵌入式系统，这些系统无法从理论上理解，导致现代嵌入式系统工程师的设计工具不足。嵌入式系统需要开发新的理论、方法和工具，以提供对这些系统的正确理解，并加速分析和设计方法，以确保安全性，同时也大大减少其设计时间。嵌入式系统需要非常新颖、非常具有挑战性的规范，这些规范必须处理不同任务的同步、排序和时间顺序。在控制理论中，用传统的数学公式是无法实现这种期望规格的数学表述的。另一方面，计算机辅助验证推广了几种时间逻辑来描述复杂规范的使用。然而，重点一直是对纯离散系统的这些性质的验证，而不是对具有连续组件的系统的综合。本文研究了一种自动合成混合控制器的新方法，以满足以时间逻辑表示的规范。特别是，开发了方法来提取线性控制系统的有限抽象，这将用于设计满足所需时间逻辑规范的控制器。与其他方法相反，该项目考虑了与连续动态系统相反的连续控制系统的依赖于规范的抽象。所提出的框架将为离散控制器的计算提供算法和工具，通过改进将为原始系统提供嵌入式混合控制器，同时提供性能和正确性保证。该提案的教育议程侧重于跨部门、本科、信号和系统课程的发展，该课程拓宽了系统的定义，以便在传统控制或通信系统之外捕获软件和硬件系统。本课程与最近的课程变化相协调，旨在离散和连续世界中信号和系统概念的教育一致性。

LGORITHMIC SYNTHESIS OF EMBEDDED CONTROLLERSIn recent years, microprocessors have invaded the physical world, resulting in sophisticated but complicated networked embedded systems that defy theoretical understanding, resulting in inadequate design tools for the modern embedded system engineer. Embedded systems require the development of new theories, methods, and tools providing the correct understanding of these systems andaccelerated analysis and design methods in order to ensure safetybut also substantially decrease their design time. Embedded systems require very novel, very challenging specifications that have to deal with synchronization, sequencing, and temporal ordering of differenttasks. Mathematically formulating such desired specifications cannot be achieved using traditional mathematical formulations in control theory. On the other hand, computer aided verification has popularized the use of several temporal logics to describe complex specifications. However, the emphasis has been on verification of these properties for purely discrete systems, and not on synthesis for systems with a continuous component.In this research, a novel approach for automatically synthesizing hybrid controllers is pursued in order to satisfy specifications that are expressed in temporal logics. In particular, methodologies are developed to extract finite abstractions of linear control systems, that will be used to design controllers meeting the desired temporal logic specifications. Contrary to other approaches, this project considers specification dependent abstractions for continuous control systems as opposed to continuous dynamical systems. The proposed framework will provide algorithms and tools for the computation of discrete controllers, which by refinement will lead to embedded, hybrid controllers for the original system while providing performance and correctness guarantees.The educational agenda of the proposal focuses on the development of a cross-departmental, undergraduate, signals and systems course that broadens the definition of systems in order to capture software and hardware systems in addition to traditional control or communication systems. This course has been carefully coordinated with recent curriculum changes and aims at the educational uniformity of signals and systems concepts in both the discrete and the continuous world.