Self-Driving Vehicle Verification Towards a Benchmark

Understand

Industrial cyber-physical systems are hybrid systems with strict safety requirements.

• Despite not having a formal semantics, most of these systems are modeled using Stateflow/Simulink for mainly two reasons: (1) it is easier to model, test, and simulate using these tools, and (2) dynamics of these systems are not supported by most other tools.
• Furthermore, with the ever growing complexity of cyber-physical systems, grows the gap between what can be modeled using an automatic formal verification tool and models of industrial cyber-physical systems.
• In this paper, we present a simple formal model for self-deriving cars.