Verification of Camera-Based Autonomous Systems

We consider the problem of verifying the safety of the trajectories of a camera-based autonomous vehicle in a given 3-D-scene. We give a procedure to verify that all trajectories starting from a given initial region reach a specified target region safely without colliding with obstacles on the way. We also give a prioritization-based falsification procedure that collects unsafe trajectories. Both our procedures are based on the key notion of image-invariant regions, which are regions within which the captured images are identical. We evaluate our methods on a model of an autonomous road-following drone in a variety of 3-D-scenes; our experimental results demonstrate the feasibility and benefits of our approach for both safety analysis and falsification.