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.
|
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. |
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).
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
-
How to install the simulated complete experiment: install.
-
How to run the regular simulation experiment: run-sim.
-
How to run the regular experiment: run-real.
-
How to produce and compile the Fiacre/Hippo version of the experiment: Fiacre/Hippo modules.
-
How to run the Fiacre/Hippo experiment in simulation with a formal model monitor: Hippo Monitor in simulation.
-
How to run the Fiacre/Hippo experiment on a real drone with a formal model monitor: Hippo Monitor on a real drone.