Difference between revisions of "Portal:Tools"

From Verification Body of Knowledge
Jump to navigation Jump to search
Line 1: Line 1:
<big>Verification of Autonomous Systems -- A Selection of Tools</big>
<big>Verification of Autonomous Systems -- A Selection of Tools and Processes </big>


== Specification & Modelling ==
== Tools ==
 
=== Specification & Modelling ===
* Modelling of Robotic Systems:  [https://www.cs.york.ac.uk/robostar/robotool/ RoboTool]
* Modelling of Robotic Systems:  [https://www.cs.york.ac.uk/robostar/robotool/ RoboTool]
* Modelling of Robotic Systems:  [https://redmine.laas.fr/projects/genom3-fiacre-template/gollum/index GenoM]
* Modelling of Robotic Systems:  [https://redmine.laas.fr/projects/genom3-fiacre-template/gollum/index GenoM]
Line 46: Line 48:
** Available on Gitlab
** Available on Gitlab
** [https://link.springer.com/chapter/10.1007/978-3-030-85248-1_15 Paper reference]
** [https://link.springer.com/chapter/10.1007/978-3-030-85248-1_15 Paper reference]
== Processes ==

Revision as of 12:26, 31 May 2022

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

Tools

Specification & Modelling

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 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

Processes