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.