Difference between revisions of "Portal:Tools"

From Verification Body of Knowledge
Jump to navigation Jump to search
Line 6: Line 6:
* Executable Agent Specifications: [https://www.csc.liv.ac.uk/~michael/TLBook/MetateM-System/ Concurrent MetateM]  
* Executable Agent Specifications: [https://www.csc.liv.ac.uk/~michael/TLBook/MetateM-System/ Concurrent MetateM]  


[[Creating Portal:Sources]]
[[Portal:Sources]]





Revision as of 12:17, 5 April 2022

Verification of Autonomous Systems -- A Selection of Tools

Specification & Modelling

Portal:Sources


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