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

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

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.