CAREER: Automated Synthesis of Embedded Control Software

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

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.