Algorithmic Synthesis of Embedded Controllers

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

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.