Portal:Tools

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

Latest technical innovations

• Verification of autonomous systems that are able to learn and adapt to their environmental conditions through testing or formal methods. Verifying autonomous systems that learn goes beyond verifying neural networks or deep learning models, a more dedicated verification topic that has started to occupy the research space for the last 5 to 10 years.
• Industrial effort on the verification of autonomous vehicles for public deployment (e.g. autonomous cars, autonomous water vehicles, and drones). This means a documented large scale application of verification tools and methods by companies.
• Specifications of large-scale autonomous systems through the richness of formal languages and ontologies. A careful balance between expressiveness and formalism is required to describe and model the wide range of behaviours of an autonomous system in the wild
• The latest version of the verification tool UPPAAL link, the tool C2E2 link, and tools mentioned in the Assured Autonomy compendium link, in particular, VerifAI, Scenic, and Overt/OvertVerify. These tools exemplify the cutting-edge innovation in Verification of Autonomous Systems.

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