Synthesis of Embedded Software from Hybrid Models

从烤面包机到手机，从汽车到飞机，嵌入式软件实现并控制设备与其环境的交互，我们的社会越来越依赖于这些设备。尽管嵌入式设备在几乎每一个工程产品中的扩散，嵌入式软件的开发仍然是一个低水平，耗时和容易出错的过程。这是因为现代编程语言抽象了时间和平台的限制，而嵌入式软件的正确性关键依赖于严格的截止日期。这项由NSF资助的研究旨在开发新的基于模型的设计和实现方法，用于合成可靠的嵌入式软件。混合系统模型，允许混合状态机为基础的离散控制与微分方程为基础的连续动态，用于设计和分析。该研究探讨了如何将这些模型映射到正确性，模块化和可移植性问题指导的代码。技术挑战包括弥合混合模型的平台无关和时间语义与由其生成的可执行软件之间的差距。这包括将控制任务的生成与调度集成，以确保最佳性能。该项目中的组件技术正在实施并集成到一个实验工具包中。一个计算机辅助输液泵控制系统，和一个无人机使用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.