Documentation for the Validation and Verification of the Drone experiment using GenoM3 and Fiacre/TINA/Hippo.

This project is showing how can one deploy formal methods to validate and verify some aspects of the navigation and the flight control of a simple drone, offline, on the components but also online, while it is running.

This project contains the instruction to install all the GenoM3 components and scripts to run the experiment on a real drone or with a Gazebo based simulator. Note, that the same GenoM3 components are used on both setup.

Note The credits for the drone experiment (components and simulation) go to Anthony Mallet, Martin Jacquet, Dario Sanalitro, etc and other people from the RIS/LAAS team, we are merely using their GenoM3 components and setup as an example of experiment which can be harnessed with formal V&V tools.
The setup for the real drone

A similar setup with Gazebo. Note that one need to install plugin to Gazebo to simulate the drone flight, and to emulate the motion capture (optitrack).

The setup for the Gazebo Simulation

GenoM3 components

All GenoM3 components are available under robotpkg and are described in their respective project:

  • rotorcraft Low level hardware controller.

  • nhfc Near-hovering flight controller.

  • maneuver Simple maneuver planner for aerial robots.

  • pom GenoM3 component for localization. This component collects position/velocity/acceleration measurements from other components, and generate a fused state estimation from these sources.

  • optitrack GenoM3 component exporting motion capture data from an Optitrack system.

The figures above show all the components as well as their ports (produced by the component they are attached to, and read by the component(s) with an arrow pointing to the port). For example the pose port is produced (written) by pom and read (used) by maneuver and nhfc.

Installation and running