Portal:Tools

Verification of Autonomous Systems -- A Selection of Tools and Processes

Tools

Specification & Modelling

• Modelling of Robotic Systems: RoboTool
• Modelling of Robotic Systems: GenoM
• Executable Agent Specifications: Concurrent MetateM (not maintained)

Title 1

Formal Verification

• Program model-checking of agent-based Autonomous Systems: MCAPL
• Robustness analyzer for Neural Networks: ERAN
• SMT solver for Neural Networks: Marabou
• Theorem prover for Cyber-Physical Systems: KeYmaera X

Software Testing

• Conformance testing of Cyber-Physical Systems: HyConf

Concolic Testing

Concolic testing alternates between concrete examples and symbolic analysis.

• Concolic testing for Deep Neural Networks: DeepConcolic

Physical Testing

• Physical integration testing for ROS 2: ROSPIT

Runtime Verification

• Runtime verification for Robot Operating System (ROS): ROSMonitoring
• Runtime verification of Robotic Systems: Varanus
• Runtime verification for Robot Operating System (ROS): ROSRV

Multi-purpose verification tools

• Breach
  • How to write STL requirements
  • Falsification of STL requirements
  • Monitoring for STL formulae
  • Interfacing with Simulink models using the toolbox
  • Available in Github

• S-Taliro
  • Verification
  • Conformance testing
  • MATLAB toolbox

• PSY-Taliro
  • Python toolbox for S-Taliro
  • Available on Gitlab
  • Paper reference

Processes

• Model after the Guide on VAS but more detailed
• Refer to standards on verification processes (double V model, software verification, cybersecurity(?), assurance cases, etc.)
• This can link back to tools sections