CAREER: Automated Synthesis of Embedded Control Software

这个NSF CAREER项目代表了对嵌入式控制软件的开发，是正确的设计的努力。追求这一雄心勃勃的目标依赖于新颖的想法，通过将控制与软件设计相结合，促进嵌入式软件设计的范式转变。特别地，通过使用连续控制系统的有限抽象，控制理论思想正被应用于执行动态约束（控制）、软件约束（例如，共享资源、实时属性）和硬件约束（例如，功耗、执行时间）。除了减轻测试和正式验证的需要，这项研究还开发了自动化合成方法，允许更快的设计周期和嵌入式应用程序的功能和复杂性的增加。这种嵌入式控制软件设计的正确构建方法具有直接的技术，经济和社会后果，这些后果由软件开发时间和成本的减少引发。此外，该项目的研究成果也有助于提高大型嵌入式系统网络的功能性、鲁棒性和可靠性，这些系统正在成为我们社会的重要基础设施。对研究生和本科生教育的重要贡献补充了该项目的研究部分。一个新的研究生课程验证和嵌入式控制系统的合成正在提供在圣母院。支持这门课程的课堂讲稿将被出版，以进一步传播在这个项目的背景下开发的新思想，并促进在其他大学创建类似的课程。圣母大学的本科教育正在通过本科生参与研究和修订电气网络入门课程的实验部分得到改善，以便使电气工程二年级学生熟悉嵌入式系统和嵌入式编程的基本技能。

This NSF CAREER project represents an effort towards the development of embedded control software that is correct by design. The pursuit of this ambitious objective relies on novel ideas fostering a paradigm shift in embedded software design by integrating control with software design. In particular, through the use of finite abstractions of continuous control systems, control theoretic ideas are being applied to the design of software enforcing dynamic constraints (control), software constraints (e.g., shared resources, real-time properties) and hardware constraints (e.g., power consumption, execution times). In addition to alleviating the need for testing and formal verification this research is also developing automated synthesis methods allowing for faster design cycles and an increase in functionality and complexity of embedded applications. This correct by construction approach to embedded control software design has immediate technological, economical and societal consequences triggered by a reduction in software development time and cost. Furthermore, the research outcome of this project is also contributing to the advancement in functionality, robustness and dependability of the large networks of embedded systems that are becoming essential infrastructures of our society. Important contributions to graduate and undergraduate education complement the research component of the project. A new graduate course on verification and synthesis of embedded control systems is being offered at Notre Dame. The lecture notes supporting this course will be published to further disseminate the novel ideas developed in the context of this project and to promote the creation of similar courses in other universities. Undergraduate education at Notre Dame is being improved through the participation of undergraduate students in research and by revising the laboratorial component of the introductory course to electrical networks in order to familiarize second year electrical engineering students with embedded systems and basic skills in embedded programming.