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.
Society is increasingly reliant on embedded, networked systems that are used in transportation, healthcare, civil infrastructure, and many more areas of critical importance. These systems are reactive, i.e.,their correctness is defined by an ongoing interaction with the surrounding environment. The objective of this CAREER project was to improve the dependability and robustness of reactive systems by developing an integrated approach to verification by combining formal methods and machine learning. A particular focus was on applications to the design of real-time embedded systems and networked systems. To this end, the project included the following major accomplishments: (i) Intellectual Merit: On the theoretical side, a new formal framework was developed for combining inductive machine learning with deductive formal methods. This approach, termed sciduction, generalizes from several specific results obtained in the project for particular applications. One such problem is the verification of timing properties of embedded software. The project developed GameTime, a new approach to timing analysis that combines game-theoretic online learning with systematic test generation based on satisfiability solving (see attached image showing the GameTime tool flow). GameTime has been applied to industrial control software in automotive applications, is publicly available, and was presented at an invited tutorial at the Design Automation Conference. Another problem concerned the synthesis of programs and controllers from observations of their input-output behavior. The project developed new methods to synthesize programs and control strategies from such input-output observations by combining learning algorithms with procedures for satisfiability solving or numerical simulation. (ii) Broader Impact: The project helped support development of a new undergraduate course on Embedded Systems at UC Berkeley. The PI also co-authored a textbook, "Introduction to Embedded Systems --- A Cyber-Physical Systems Approach" for this undergraduate course (see attached image of book cover). The textbook, which is freely available online, and the associated course curriculum have been very successful at Berkeley and have been widely adopted at universities in the U.S. and abroad. Additionally, the project helped train several graduate and undergraduate students. Further, undergraduate students from around the U.S. in the SUPERB summer outreach program at UC Berkeley have been contributors to research conducted in this project. The PI has also disseminated results obtained in the project to a broader audience through tutorials and invited talks, and disseminated the educational material to a global audience by teaching a massive open online course on Cyber-Physical Systems on the edX platform. In summary, given the increasing pervasiveness and importance of cyber-physical systems in our societal infrastructure, the theory, techniques, and tools developed in this project provide steps to increase their dependability and robustness, and to help train the next generation of scientists and engineers design high-quality cyber-physical systems.
