Tutorial / Case Studies

This page describes how to run many of the examples included in the VerifAI repository, which illustrate the main use cases of VerifAI. After cloning the repository, you can install the extra dependencies needed for the examples by running:

python -m pip install -e ".[examples]"

Emergency Braking with a simple Newtonian simulator

Scenic comes with a simple built-in Newtonian physics simulator, which supports running traffic scenarios. In this example scenario we have a car (in red) whose task is to stay within its lane using a PID controller, while maintaining a safe distance of 5 meters to objects in front.

Task: Falsify the PID lane keeping controller

Sample space: distance from ego to obstacle

Relevant files:

examples/scenic/falsify_distance.py : Defines type of falsifier (sampler and number of iterations)
examples/scenic/newtonian/carlaChallenge2.scenic : Scenic program defining the ego vehicle’s behavior (i.e. policy) and its environment

Running the falsifier: To run this example go to examples/scenic. Then run python falsify_distance.py.

The falsifier runs for 5 iterations by default; you can change this by modifying n_iters in falsify_distance.py.

Expected Output: During the running of the falsifier you should see a top-down view of the simulations taking place. When falsification has completed, the script will print out tables listing all of the samples that were generated and the associated satisfaction value of the specification, rho. Rho represents the quantitative satisfaction of the specification such that the sample satisfies the specification if rho is positive and violates the specification if rho is negative. The samples are separated into two tables, the error_table for counterexamples to the specification and the safe_table for all other samples.

Learning More: See the README in the examples/scenic folder for more options the falsify_distance.py script supports, including running similar experiments in the CARLA driving simulator.

Lane keeping with inbuilt simulator

VerifAI comes with an inbuilt simulator developed from this car simulator. In this example we have a car (in red) whose task is to stay within its lane using an LQR controller.

Task: Falsify the LQR lane keeping controller

Sample space: Initial x-position, angle of rotation, and cruising speed.

Relevant files:

src/verifai/simulators/car_simulator/examples/lanekeeping_LQR/lanekeeping_falsifier.py : Defines the sample space and type of falsifier (sampler and number of iterations)
src/verifai/simulators/car_simulator/examples/lanekeeping_LQR/lanekeeping_simulation.py : Defines the controller and the simulation environment

Running the falsifier: To run this example open two terminal shells and go to src/verifai/simulators/car_simulator in each of them. Then in first one run python examples/lanekeeping_LQR/lanekeeping_falsifier.py and wait till you see “Server ready” in the terminal; then run python examples/lanekeeping_LQR/lanekeeping_simulation.py in the other one.

The falsifier runs for 20 iterations, you can change this by modifying MAX_ITERS in examples/lanekeeping_LQR/lanekeeping_falsifier.py. At the end of the runs, you should see “End of all simulations” in the terminal where you ran python examples/lanekeeping_LQR/lanekeeping_simulation.py.

Expected Output: During the running of the falsifier you should the samples and the associated value of the specification satisfaction (rho). Rho represents the quantitative satisfaction of the specification such that the sample satisfies the specification if the rho is positive or falsifies the specification if the rho is negative.

You should see two tables in the first terminal where you ran python examples/lanekeeping_LQR/lanekeeping_falsifier.py, labeled Falsified Samples a collection of all falsified samples and Safe Samples a collection of all the samples which were safe.

Data augmentation

In this example we try to falsify a Neural Network (NN) trained to detect images of cars on roads. We re-create the data augmentation example from this paper. We implemented our own picture renderer which generates images by sampling from a low dimensional modification (sample) space.

Task: Falsify the NN trained on the synthetic images generated by the picture rendered

Sample space: Image background (37 backgrounds), number of cars- (x, y) position and type of car, overall image brightness, color, contrast, and sharpness.

Relevant files:

examples/data_augmentation/falsifier.py : Defines the sample space and type of falsifier (sampler and number of iterations)
examples/data_augmentation/classifier.py : Interface to the picture renderer and instantiate the NN

Running the falsifier: Open two terminal shells and go to examples/data_augmentation in each of them. Then in first one run python falsifier.py and wait till you see “Server ready” in the terminal; then run python classifier.py in other one.

The falsifier runs for 20 iterations, you can change this by modifying MAX_ITERS in examples/data_augmenatation/falsifier.py. At the end of the runs, you should see “End of all classifier calls” in the terminal where you ran python classifier.py.

The falsifying samples are stored in the data structure error_table. We can further analyse the error_table to generate images for retraining the NN. We have introduced three techniques to generate new images for the NN re-training:

Randomly sample samples from the error_table
Top k closest (similar) sampler from the error_table
Use the PCA analysis on the samples to generate new samples

Expected Output: During the running of the falsifier you should the samples and the associated value of the specification satisfaction (rho). Here rho represents the qualitative (boolean) satisfaction. Its True if the NN correctly classifies the image.

You should see a table labeled Error Table a collection of all falsified samples in the first terminal where you ran python falsifier.py. This follows two counterexample sets, one randomly generated from the error table and the other with k closest samples. We set k = 4 in this example. This is followed by the PCA analysis results, we report the pivot and the 2 principle components.

The images in the two counterexample sets will pop up at the end of the run. The images are saved in the counterexample_images folder. The images with the prefix “random_” are from the random samples counterexample set and those with the prefix “kclosest_” are from the k closest counterexample set.

Webots examples

To run these examples you need to download and install Webots 2018 from here. Webots 2018 is not free software, however you can get a 30-day free trial. While choosing license please select PRO license. When you open Webots for the first time go to Webots->Preferences and change Startup Mode to Pause.

(It should be possible to adapt these examples to work under the newer open-source versions of Webots as well; mainly, the .wbt files need to be regenerated using the Webots OSM Importer.)

We do not currently support using Webots 2019 (even though it is free software), since we found its performance to be very poor on machines without GPUs (e.g. personal laptops).

Scene Generation using Scenic

In this example we use the probabilistic programming language Scenic to generate scenes where a road is obstructed by a broken car behind traffic cones. The scene we would like to generate is made up of an ego car (in red) and a broken car (in silver) parked behind three traffic cones.

Task: Generate scenes using Scenic

Sample space: Position of the ego car in the city, position and orientation of the cones, position and orientation of the broken car

Relevant files:

examples/webots/controllers/scenic_cones_supervisor/lane_cones.scenic : Scenic code to generate scenes
examples/webots/controllers/scenic_cones_supervisor/scenic_cones_sampler.py : Interface to scenic
examples/webots/controllers/scenic_cones_supervisor/scenic_cones_supervisor.py : Interface to webots
examples/webots/worlds/shattuck_build.wbt : Webots world of downtown Berkeley

Running the sampler: Launch Webots and load the world examples/webots/worlds/shattuck_build.wbt (File->Open World). Open a terminal and go to examples/webots/controllers/scenic_cones_supervisor and run python scenic_cones_sampler.py. Once that starts running (you will notice a message “Initialized Sampler” in the terminal), you can start the simulation.

The sampler runs for 20 iterations, you can change this by modifying MAX_ITERS in examples/webots/controllers/scenic_cones_supervisor/scenic_cones_sampler.py. At the end of the runs, you should see “End of scene generation” in the Webots console and the Webots window closes.

Expected Output: During the running of the sampler you should the samples and the associated value of the specification satisfaction (rho). Since in this application we focus only on scene generation, rho does not have any practical relevance (and has been set to infinity).

You should see the collection of all samples generated by the scenic script in the terminal where you ran python scenic_cones_sampler.py.

Falsification of accident scene with cones

In this example we choose a scene generated from the above case study and run our falsifier to find small variations in the initial scene variation which lead to the ego car (in red) to crash into the traffic cones. For this purpose, we fix the location of the broken car, cones, and the ego_car but introduce variations in the color of the broken, and noise in the position and orientation of the ego car, cones and the broken car.

The ego car’ controller is responsible for safely maneuvering around the cones. To achieve this, we implemented a hybrid controller. Initially, the car tries to remain in its lane. The controller in the ego car relies on a NN we trained to detect the cones and estimate the distance to the cones. When the distance to the cone is less than 15 meters the car starts a lane changing maneuver. This can be seen as the NN warning a human in the car to change lanes. To capture the human behavior, we introduce a reaction time (which is also a parameter) of the human.

Task: Falsify the NN detecting cones and the hybrid controller

Sample space: Initial position and orientation noise of the ego car, cruising speed of the ego car, position and orientation noise in the broken car, position error and orientation of the cones, color of the broken car, reaction time of the human

Relevant files:

examples/webots/controllers/cones_lanechange_supervisor/cones_lanechange_falsifier.py : Defines the sample space and type of falsifier (sampler and number of iterations)
examples/webots/controllers/cones_lanechange_supervisor/cones_lanechange_supervisor.py : Interface to webots
examples/webots/worlds/shattuck_buildings_falsif.wbt : Webots world of downtown Berkeley

Running the falsifier: During the running of the falsifier you should the samples and the associated value of the specification satisfaction (rho). Rho is the quantitative satisfaction.

Launch Webots and load the world examples/webots/worlds/shattuck_buildings_falsif.wbt (File->Open World). Open a terminal and go to examples/webots/controllers/cones_lanechange_supervisor and run python cones_lanechange_falsifier.py. Once that starts running (you will notice a message “Initialized Sampler” in the terminal), you can start the simulation.

The falsifier runs for 20 iterations, you can change this by modifying MAX_ITERS in examples/webots/controllers/cones_lanechange_supervisor/cones_lanechange_falsifier.py. At the end of the runs, you should see “End of simulations” in the Webots console and the Webots window closes.

Each simulation run takes about 16 seconds in the simulation time; but may take more time in real time because of overheads like the neural networks calls and rendering.

Expected Output: You should see a table Unsafe Samples the collection of all samples generated that caused the ego car to crash into the cones in the terminal where you ran python cones_lanechange_falsifier.py.

Fuzz testing using Scenic

In this example we use Scenic to initial conditions to recreate collision scenarios at an intersection. In this example, the ego car (in green) if going straight through an intersection. The front view of the ego car is obstructed by a set of cars (in silver) which are stopped at the intersection. A human car (in red) attempts to the take a left turn at the intersection. In this scenario, the camera of both the ego car and the human car are obstructed by the silver cars standing at the intersection. We use scenic to sample the initial positions and orientations of the ego car, human car and couple of the standing cars at the intersection.

To reduce the chances of collision, we designed a controller for the ego car which utilizes the information coming from a “smart intersection”. The smart intersection sends a warning to the ego car, when the human car approaches the intersection. Based on how early the warning comes in, we reduce the number of collision scenarios.

Task: Generate accident scenarios and test controllers with “smart intersection”

Sample space: Position and orientation of the ego car, human car and standing cars

Relevant files:

examples/webots/controllers/scenic_intersection_supervisor/intersection_crash.scenic : Scenic code to generate scenes
examples/webots/controllers/scenic_intersection_supervisor/scenic_intersection_sampler.py : Interface to scenic
examples/webots/controllers/scenic_intersection_supervisor/scenic_intersection_supervisor.py : Interface to webots
examples/webots/worlds/scenic_intersection.wbt : Webots world of the intersection

To run this example, you need to install pyproject, $pip install pyproj

Running the sampler: Launch Webots and load the world examples/webots/worlds/scenic_intersection.wbt (File->Open World) . Open a terminal and go to examples/webots/controllers/scenic_intersection_supervisor and run python scenic_intersection_sampler.py. Once that starts running (you will notice a message “Initialized Sampler” in the terminal), you can start the simulation.

To test the original scenario without the smart intersection, ensure that ignore_smart_intersection = True on line 24 in the file examples/webots/controllers/smart_brake/smart_brake.py. To test with smart intersection set ignore_smart_intersection = False. You can update how early the warning is sent by updating the value of intersection_buffer in line 111 in scenic_intersection_supervisor.py. If set to 0, then the warning is given only when the human car enters the intersection. If > 0, the warning is sent when the car is some distance away from the intersection. If < 0, the warning is sent when the car is some distance inside the intersection.

The sampler runs for 20 iterations, you can change this by modifying MAX_ITERS in examples/webots/controllers/scenic_intersection_supervisor/scenic_intersection_sampler.py. At the end of the runs, you should see “End of accident scenario generation” in the Webots console and the Webots window closes.

Each simulation run takes about 16 seconds in the simulation time; but may take more time in real time because of overheads like rendering and communication between controllers.

Expected Output: During the running of the sampler you should the samples and the associated value of the specification satisfaction (rho). Since in this application we focus only on scenario generation, rho does not have any practical relevance (and has been set to infinity).

You should see the collection of all samples generated by the scenic script in the terminal where you ran python scenic_intersection_sampler.py.

OpenAI Gym examples

The following two examples require the baselines package, which does not support TensorFlow 2 (needed for other examples above), so they cannot be easily run at the moment. We leave them here since they were discussed in the VerifAI paper and provide examples of how to use VerifAI with reinforcement learning algorithms. We would welcome a pull request updating them to use an RL library which is actively maintained!

These examples require at least version 0.1.6 of the baselines package. As of May 2020, the version on PyPI is too old and will not work, so you need to install baselines from its repository. Follow the installation instructions given there, remembering to first activate your virtual environment if necessary.

Cartpole

In this example we want to test the robustness of a controllers to changes in model parameters and initial states of the cartpole from openAI gym.

We use OpenAI baselines to train a NN to control the cartpole . We train a NN using Proximal Policy Optimization algorithms (PPO) with 100000 training episodes.

We use the reward function as the specification for testing; i.e., if the reward is positive for all the environments the controller is safe. For the cartpole, the specification is: the maximum variation of the pole from the center should be less than 12 degree and maximum variation of the initial position should be less than 2.4m. To test the controller we loosen the training thresholds for angle, by 0.01 radians, and the x variation, by 0.1m, to get the testing thresholds. To capture this we define a specification using metric temporal logic python library which VerifAI can convert into a monitor internally.

Task: Test the robustness of the NN controller trained using PPO

Sample space: Initial state x position and rotation of the cartpole, model parameters - mass and length of pole and mass of the cart

Relevant files:

examples/openai_gym/cartpole/cartpole_falsifier.py : Defines the sample space and type of falsifier (sampler and number of iterations)
examples/openai_gym/cartpole/cartpole_simulation.py : Interface to OpenAI gym and baselines

Running the falsifier: During the running of the falsifier you should the samples and the associated value of the specification satisfaction (rho). Rho is the quantitative satisfaction.

Open two terminal shells and go to cd examples/openai_gym/cartpole in each of them. Then in first one run python cartpole_falsifier.py and wait till you see “Initialized sampler” in the terminal; then run python cartpole_simulation.py in other one.

The falsifier runs for 20 iterations, you can change this by modifying MAX_ITERS in examples/openai_gym/cartpole/cartpole_falsifier.py. At the end of the runs, you should see “End of all cartpole simulations” in the terminal where you ran python cartpole_simulation.py.

Expected Output: During the running of the falsifier you should the samples and the associated value of the specification satisfaction (rho). Rho is the quantitative satisfaction.

You should see the error table Counter-example samples containing all falsified samples in the terminal where you ran python cartpole_falsifier.py

Mountaincar

In this example we show the effect of hyper-parameters to train NN to control the mountaincar environment from openAI gym.

Specifically, we see the effects of different training algorithms and size of the training set on synthesizing a NN controller.

We treat the reward function provided by the environment as our specification. For the mountaincar, this is characterized by the distance to the flag. Here, unlike the previous examples, we would like to find the set of parameters which which ensures the NN is able to correctly control the mountaincar. To do this, we negate the specification so that falsifying the specification implies finding a safe controller.

Task: Study the effect of hyperparameters in training NN controllers for mountaincar

Sample space: Training algorithms - Deep RL algorithms, number of training episodes

Relevant files:

examples/openai_gym/mountaincar/mountaincar_falsifier.py : Defines the sample space and type of falsifier (sampler and number of iterations)
examples/openai_gym/mountaincar/mountaincar_simulation.py : Interface to OpenAI gym and baselines

Running the falsifier: During the running of the falsifier you should the samples and the associated value of the specification satisfaction (rho). Rho is the quantitative satisfaction.

Open two terminal shells and go to cd examples/openai_gym/mountaincar in each of them. Then in the first one run python mountaincar_falsifier.py and wait till you see “Initialized sampler” in the terminal; then run python mountaincar_simulation.py in the other one.

The falsifier runs for 20 iterations, you can change this by modifying MAX_ITERS in examples/openai_gym/mountaincar/mountaincar_falsifier.py. At the end of the runs, you should see “End of all mountaincar simulations” in the terminal where you ran python mountaincar_simulation.py.

Expected Output: You should see a table Hyper-parameters leading to good controllers containing all sampled hyperparamaters which build NN which can safely control the mountaincar in the terminal where you ran python mountaincar_falsifier.py.