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.