CAREER: Robust Reactive Systems through Verification and Learning

我们对嵌入式和网络反应系统的依赖正在迅速增长。然而，日益增加的复杂性和较短的发布周期使得部署没有设计错误和程序错误的系统变得更加困难。 这些系统在无人监督的环境中运行，或者在高可用性要求下运行，在这种情况下，尽最大努力修补错误是不够的。 传统的离线缺陷查找技术虽然有帮助，但扩展性差，成本极高，并且由于环境模型不精确而可能无效。 在线验证有可能缓解这些问题，但它增加了性能开销，并且没有已知的技术可以从一般类型的错误中恢复系统。NSF CAREER研究旨在通过结合离线和在线验证和学习来解决这些问题，以便在运行时检测和纠正错误。长期研究目标是开发一种集成的验证方法，以提高反应式系统对设计错误和程序错误的鲁棒性。在理论方面，该项目正在开发算法技术和正式框架，用于从设计错误中恢复反应式系统。目前正在研究结合离线和在线分析的新技术。正在探索使用在线和离线学习来随着时间的推移自我进化系统。拟议的工作可以提高工业生产力，提高系统的可用性，减少系统管理开销，并处理无人监督的设置和不可预测的环境。项目工作主要集中在两个方面：实时嵌入式系统和网络化系统。 该项目的教育和推广部分包括开发嵌入式系统的本科课程，沿着学生通过大学推广方案参与研究项目。

Our reliance on embedded and networked reactive systems is growing rapidly. However, increasing complexity and short release cycles make it harder to deploy systems that are devoid of design errors and program bugs. These systems operate in unsupervised settings or under high-availability requirements, where best-effort patching of bugs does not suffice. Conventional offline bug-finding techniques help, but scale poorly, have extremely high cost, and can be ineffective due to imprecise environment models. Online verification has the potential to mitigate these problems, but it adds a performance overhead and no techniques are known to recover systems from a general class of errors. This NSF CAREER research seeks to address these problems by combining offline and online verification and learning, in order to detect and correct errors at run time.The long-term research goal is to develop an integrated approach to verification to improve the robustness of reactive systems to design errors and program bugs. On the theoretical side, this project is developing algorithmic techniques and a formal framework for recovering reactive systems from design errors. Novel techniques for combining offline and online analyses are being investigated. The use of online and offline learning for self-evolving a system over time are being explored. The proposed work can improve industrial productivity by enhancing system availability, reducing system administration overheads, and handling unsupervised settings and unpredictable environments. The project work mainly focuses on two areas: real-time embedded systems and networked systems. The project's education and outreach component includes developing an undergraduate curriculum on embedded systems, along with involvement of students in research projects through university outreach programs.