Predictable Autonomy for Cyber-Physical Systems

Cyber-physical systems combine complex physics with complex software. Although these systems offer significant potential in fields such as smart grid design, autonomous robotics and medical systems, verification of CPS designs remains challenging. Model-based design permits simulations to be used to explore potential system behaviors, but individual simulations do not provide full coverage of what the system can do. In particular, simulations cannot guarantee the absence of unsafe behaviors, which is unsettling as many CPS are safety-critical systems.The goal of set-based analysis methods is to explore a system's behaviors using sets of states, rather than individual states. The usual downside of this approach is that set-based analysis methods are limited in scalability, working only for very small models. This talk describes our recent process on improving the scalability of set-based methods, where the states are in some Euclidean space. We describe linear star sets, a new spatial data structure that we used to verify properties about linear time-invariant hybrid automata with many (up to one billion!) coupled continuous state variables. Lastly, we discuss using linear star sets to perform set-based input/output verification of neural networks.