Position: Ph.D. Candidate and Research Assistant
Current Institution: University of Illinois at Urbana-Champaign
Verifying and Debugging Smart Cyber-physical Systems
The 21st century has been witnessing a phenomenal growth in cyber-physical systems (CPS), which tightly couple physical processes with software, networks, and sensing. Unmanned aerial vehicles are starting to share increasingly crowded airspace with commercial and passenger air traffic, autonomous satellites will soon coordinate with one another and service aging satellites, networked medical devices are being implanted, ingested, and injected in humans, and tomorrow’s cars may drive themselves. Reliability and security lapses of such cyber-physical systems routinely disrupt communities, and on many occasions have led to catastrophic failures, with major damage to infrastructure and people. Fortunately, recent advances in verification tools for nonlinear hybrid systems have brought them to the threshold of solving real-world embedded system design and analysis problems. Early successful applications have been demonstrated in automotive powertrain control systems, medical devices, and power plants.
A common way to model cyber-physical systems is as hybrid systems or networks. Current testing and debugging approaches for CPS in the industry are best-effort at best. A test suite covers a small fraction of behaviors. It is attractive because its computational burden is lower and it requires only executable models which are often available from the design, but it suffers from incompleteness. This leaves out many other behaviors untested which can later appear as serious bugs. Formal verification techniques, on the other hand, provide a mathematical proof that the system behaves in a safe manner or has an invariant for all (possibly infinite) initial configurations or parameters of the system.
Despite the recent success of existing approaches in analyzing hybrid and embedded systems, several challenges remain to its widespread applicability: they are either applicable to only restricted classes of systems, overly conservative, or computationally expensive. The method I will present is about overcoming these challenges and computing system-level guarantees from traces for large nonlinear hybrid systems. It enables the rapid safety or invariance verification that has been demonstrated to scale to industrial designs. The key insight that enables the method to overcome the technical challenges is that it combines the speed of numerical simulations with automatic analysis of design models. I will also introduce the core algorithms of our method which automatically compute the reachable states of the system using simulations as guidance, while preserving the original soundness and relative completeness guarantees.
We have also developed the award winning tool Compare Execute Check Engine (C2E2) which implements this verification technique. C2E2 has successfully been applied for verifying the invariance of various sophisticated hybrid systems: a suite of powertrain control systems from Toyota, medical devices in conjunction with models of human physiology, a parallel aircraft landing protocol from NASA, etc.
I am Chuchu Fan, a Ph.D. candidate in the department of ECE at the University of Illinois at Urbana-Champaign, working as a research assistant in Prof. Sayan Mitra’s group since 2013. Concurrently, I am the technical director and principal investigator of a startup company, Rational Cyphy Inc., leading a group to develop software for certifying and debugging cyber-physical systems like Driver Assistance and Automated Driving systems. Before joining Prof. Mitra’s group, I received my Bachelor of Science degree in 2013 with the highest honor in the Department of Automation from Tsinghua University, Beijing. I also worked as a visiting scholar in Prof. Laurent Itti’s group at the University of Southern California in 2012. I am the recipient of several prestigious awards including the Rambus Fellowship (2016), Best Verification Result Award in CPS Week (2015), Soar Foundation Fellowship (2012) and Samsung Fellowship (2011).
I have been working on cyber-physical systems by developing and applying formal verification methods to them. My research mainly focuses on providing formal guarantees on 1) invariant verification/falsification and 2) closeness relationship among serial models, which are two important and pervasive aspects of cyber-physical systems. My work has been published and presented at several top academic conferences, for example, Computer Aided Verification (CAV 2014, 2015, 2016), Automated Technology for Verification and Analysis (ATVA 2015), Cyber-Physical Week (CPS Week 2015), Embedded Software (EMSOFT 2016). Specifically, my work on verifying Toyota’s Powertrain controller received the Robert Bosch Most Promising Verification Result at CPS Week 2015. I have also published my findings in several academic journals: IFAC Nonlinear Analysis: Hybrid Systems (2016), IEEE Design & Test (2015), and IEEE Signal Processing Letters (2013). Meanwhile, I serve as the reviewer and sub-reviewer for several international conferences and workshops on cyber-physical systems and formal methods. I am also one of the developers of the formal verification tool Compare Execute Check Engine.
I have gained much industrial experience through several internships: I worked as a research intern at Toyota Technical Center in 2015, where I collaborated with the model-based design group on advanced techniques to verify the safety of large-scale embedded systems in vehicles; in 2012, I worked at Microsoft Research in Asia as an intern in the mobile and sensing systems group, during which I earned a lot of knowledge on developing embedded software for mobile phones.
I have been active on academic communication activities as well. I am a selected participant of the French-American Doctoral Exchange Seminar in 2016 and CRA-Women Grad Cohort Workshop. I also served as the vice president of the Students Association of Science and Technology in Tsinghua Unversity for 2 years.