Synthesis of Embedded Software from Hybrid Models

从烤面包机到手机，从汽车到飞机，嵌入式软件实现并控制设备与环境的交互，我们的社会越来越依赖这样的设备。尽管嵌入式设备在几乎所有的工程产品中都在激增，但嵌入式软件的开发仍然是一个低水平、耗时和容易出错的过程。这是由于现代编程语言从时间和平台限制中抽象出来的事实，而嵌入式软件的正确性关键依赖于硬期限。这项由美国国家科学基金会资助的研究旨在开发新的基于模型的设计和实现方法，用于合成可靠的嵌入式软件。混杂系统模型允许将基于状态机的离散控制与基于微分方程的连续动态相混合，用于设计和分析。该研究探索了在正确性、模块化和可移植性问题的指导下将这些模型映射到代码的方法。技术挑战包括弥合混合模型的平台无关和定时语义与由此生成的可执行软件之间的差距。这包括将控制任务的生成与调度相结合，以确保最佳性能。正在实施该项目中的组件技术，并将其整合到一个用于实验的工具包中。选择计算机辅助输液泵控制系统和使用Piccolo航电板的无人机作为目标平台，验证了该方法的可行性和效益。

From toasters to cell phones and from cars to airplanes, embedded software implements and controls interactions of devices with their environment, and our society is increasingly relying on such devices. Despite the proliferation of embedded devices in almost every engineered product, development of embedded software remains a low level, time consuming and error prone process. This is due to the fact that modern programming languages abstract away from time and platform constraints, while correctness of embedded software relies crucially on hard deadlines. This NSF-funded research aims at developing novel model-based design and implementation methodology for synthesizing reliable embedded software. Hybrid systems models, which allow mixing state-machine based discrete control with differential equation based continuous dynamics, are used for design and analysis. The research explores ways of mapping such models to code guided by correctness, modularity and portability issues. Technical challenges include bridging the gap between the platform-independent and timed semantics of the hybrid models and the executable software generated from it. This includes integrating generation of control tasks with scheduling to ensure optimal performance. The component technologies in the project are being implemented and integrated within a toolkit for experimentation. A computer-aided infusion pump control system, and an unmanned aerial vehicle using Piccolo avionics board, are chosen as target platforms for demonstration of the feasibility and benefits of the approach.