Verification and Validation of Neural Networks in Automated Vehicles (NNV Tutorial) - E2023 IEEE IAVVC
Previous tutorial at EMSOFT'23 (Embedded Systems Week 2023)
We recommend using MATLAB Online (prior license not required!) to participate in this tutorial, but one can also use a local installation of MATLAB and NNV to follow along as well.
It is important that participants complete this section before arriving at the tutorial.
Registered participants should have received a link with a MATLAB license to use in this tutorial. If a participant has not received it, please contact the organizers.
Note: this license is not required if participants already have a valid license for all the toolboxes listed in installation instructions.
Create a copy of NNV into your MathWorks account (personal MATLAB Drive): NNV Online
- Click on
Open in MATLAB Online->Copy Folder - This will prompt you to log into your account (or register if you don’t have one)
To run NNV locally, please follow these instructions.
During this tutorial, one will learn how to represent convex sets as Star sets, load neural networks into NNV, compute reachability analysis of classification neural networks, compute the certified robustness of neural networks and more!
Setup
Open MATLAB Online (or MATLAB), then go to the directory where NNV exists on your machine (/code/nnv/), then run the startup_nnv.m script (startup_nnv.m).
Note: if you restart MATLAB, rerun startup_nnv.m, which will add the necessary dependencies to the path; you alternatively can run savepath after installation to avoid this step after restarting Matlab, but this may require administrative privileges.
-
Robustness verification on the MNIST dataset.
- Robustness verification of a single image using a model with fully-connected and ReLU layers.
- Robustness verification of a single image using a model with Convolutional, Pooling, Batch Normalization, ReLU, and fully-connected layers
- Certified robustness of a neural network classifier using a model with fully-connected and ReLU layers.
-
Robustness verification on the GTSRB dataset.
- Includes training and verification scripts as well.
-
Comparison of exact (sound and complete) and approximate (sound and incomplete) methods using Star sets exact vs approx
- Reachability analysis of an inverted pendulum.
- Safety verification example of an Adaptive Cruise Control (ACC) system.
- Training. This requires installing Simulink.
- Safety Verification.
- Safety verification of an Automated Emergency Braking System (AEBS)
- This system contains several neural networks, so a custom control loop is included in the verification script.
In addition, we have also prepared a set of exercises for the participants:
- Verification of ACAS Xu neural network with ONNX and VNNLIB files: ONNX & VNNLIB exercise
- Robustness verification of a neural network: NN exercise)
- Safety verification of a linearized plant model of an adaptive cruise control system: NNCS exercise