Available Tools and Case Studies
Program Analysis Tools
The goal is to compute symbolic post-image for controller programs in ROS for synthesizing assumptions on the interfacing variables/ROS messages.
The idea is to reuse existing program analysis tools for C++ or Python. At the best case, we only need to analyze the callback functions for ROS subscribers and the loop for periodically publishing messages using ROS publishers.
C/C++
- Software Analysis Workbench by Galois Inc. https://saw.galois.com/
- SPARTA by Facebook https://github.com/facebook/SPARTA
- IKOS by NASA https://github.com/NASA-SW-VnV/ikos
- CBMC https://github.com/diffblue/cbmc
- ESBMC https://github.com/esbmc/esbmc
Python
- CrossHair https://github.com/pschanely/CrossHair
Some Features to Look for
- How to instrument or annotate to only analyze part of a ROS package. The fewer instrumentation needed the better.
- How to add pre/post conditions or approximations for complicate/uninterpreted functions such as trigonometry functions or ellipsoids
- Floating point numbers or real numbers
- Support matrix and linear algebra?
Simulated Autonomous Systems for Case Studies
Gazebo
- Lane keeping (vision, dynamics) https://github.com/hc825b/POLARIS_GEM_e2
- Crop row following (vision) https://bitbucket.org/hc825b/terrasentia-gazebo
- Vision-based fixed-wing aircraft landing (vision, dynamics) https://github.com/cyphyhouse/Aircraft_Landing_Verification
- UTM (dynamics, coordination) https://github.com/cyphyhouse/CyPhyHouseExperiments/tree/master/experiments_utm
- ARIAC smart manufacturing (dynamics, coordination) https://github.com/cyphyhouse/ARIAC
AirSim
See https://publish.illinois.edu/aproximated-abstract-perception/
- Drone racing (vision, dynamics)
- Vision-based drone formation (vision, dynamics, coordination)