CAREER: Robust Reactive Systems through Verification and Learning

University Of California-Berkeley, Berkeley CA

Investigators

Abstract

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.