CSR - EHS: Formal Methods for Control and Real-Time Scheduling Co-Design

网络化嵌入式系统的控制提出了具有挑战性的新问题，质疑系统和控制理论中的标准假设。传统上，控制设计受益于有用的抽象，该抽象能够将控制系统的连续数学模型和反馈定律与硬件/软件以及传感器量化、采样率、实时调度等实时实现细节分离。控制回路在高度工程化的专用硬件系统中实现的普遍假设已经不再存在。网络化嵌入式系统的资源有限，大大降低了控制质量。在本项目的背景下，正在开发用于集成控制设计与实时调度的形式化方法，以克服嵌入式控制设计的这两个方面的分离所带来的一些限制。基于控制系统的新稳定性抽象，用于自动综合实时调度器执行控制、定时、正在建立调度和功耗要求。由此产生的散热器通过构造满足所需的规格，从而提供操作和性能的正式保证。该项目的结果正在评估通过实施稳定的反馈控制律云母微粒在控制工程中的两个常见的基准问题：双倒立摆，和球和beam.This控制和实时调度之间的集成允许执业工程师充分利用现有的嵌入式技术的限制，并在依赖于嵌入式硬件的行业成本降低。一个特别相关的例子是汽车行业，其中嵌入式硬件成本的小幅降低乘以大量生产的单元导致生产成本的大幅降低。

The control of networked embedded systems poses challenging new problems questioning standard assumptions in systems and control theory. Control design has traditionally benefited from a useful abstraction that enabled the separation of continuous mathematical models of control systems and feedback laws from hardware/software and real-time implementation details such as sensor quantization, sampling rates, real-time scheduling, etc. The prevailing assumption that control loops were implemented in highly engineered dedicated hardware systems can no longer be made. Networked embedded systems have limited resources that drastically reduce the quality of control. In the context of this project, formal methods for the integration of control design with real-time scheduling are being developed in order to overcome some of the limitations imposed by the separation of these two aspects of embedded control design.Based on new stability abstractions for control systems, computational tools for automated synthesis of real-time schedulers enforcing control, timing, scheduling and power consumption requirements are being built. The resulting schedulers satisfy the desired specifications by construction thus providing formal guarantees of operation and performance. The results of this project are being evaluated by implementing stabilizing feedback control laws on MICA motes for two familiar benchmark problems in control engineering: the double inverted pendulum, and the ball and beam.This integration between control and real-time scheduling allows practicing engineers to fully exploit the limits of existing embedded technology and results in cost reductions for the industry relying on embedded hardware. A particularly relevant example is the automotive industry where a small reduction in the cost of embedded hardware multiplied by the large number of produced units results in a considerable reduction in production costs.