Formal Verification of End-to-End Learning in Cyber-Physical Systems: Progress and Challenges

Autonomous systems - such as cars, planes, and trains - must come with strong safety guarantees. These systems are cyber-physical, in the sense that their safety depends crucially upon the way in which their software ("cyber") components interact with their kinetic components. Cyber-physical systems (CPS) analysis tools can verify the safety of CPS by stating correctness specifications in a formal language and then verifying - via computer-checked proof - that safety-critical software components respect these specifications. Existing approaches toward formally verifying the correctness of cyber-physical systems focus primarily on constructing formal safety proofs about classical low-dimensional models of control systems. For example, the safety of an adaptive cruise control system might be established by modeling the dynamics of two cars in terms of their positions and velocities and then proving that a control policy preserves safe separation between all cars on the road for any time horizon [15]. Researchers have employed a similar approach for ensuring the correctness of proposed FAA aircraft collision avoidance protocols [12], the European Train Control System [20], and quadcopters [21]. These proofs are typically constructed and checked using a cyber-physical systems verification tool such as Flow* [4], KeYmaera X [8], or SpaceEx [6]. CPS verification tools can provide very strong safety guarantees for cyber-physical systems, but typical techniques for using these tools rely on three assumptions that break down when applying verification techniques to real autonomous systems: 1. CPS verification techniques assume that a symbolic representation of the state of the world is known a priori. For example, formal CPS models of ground robots typically assume that the system knows the positions of all relevant obstacles, at least within some error bound [16].