Difference between revisions of "Portal:Tools"

From Verification Body of Knowledge
Jump to navigation Jump to search
Line 11: Line 11:




== Formal Verification ==
=== Formal Verification ===
* Program model-checking of agent-based Autonomous Systems:  [https://autonomy-and-verification.github.io/tools/mcapl MCAPL]
* Program model-checking of agent-based Autonomous Systems:  [https://autonomy-and-verification.github.io/tools/mcapl MCAPL]
* Robustness analyzer for Neural Networks: [https://github.com/eth-sri/eran  ERAN]
* Robustness analyzer for Neural Networks: [https://github.com/eth-sri/eran  ERAN]
Line 17: Line 17:
* Theorem prover for Cyber-Physical Systems: [http://www.ls.cs.cmu.edu/KeYmaeraX/    KeYmaera X]
* Theorem prover for Cyber-Physical Systems: [http://www.ls.cs.cmu.edu/KeYmaeraX/    KeYmaera X]


== Software Testing ==
=== Software Testing ===
* Conformance testing of Cyber-Physical Systems:  [https://github.com/hlsa/HyConf HyConf]
* Conformance testing of Cyber-Physical Systems:  [https://github.com/hlsa/HyConf HyConf]
* Concolic testing for Deep Neural Networks:  [https://github.com/xiaoweih/DeepConcolic DeepConcolic]
* Concolic testing for Deep Neural Networks:  [https://github.com/xiaoweih/DeepConcolic DeepConcolic]




== Physical Testing ==
=== Physical Testing ===
* Physical integration testing for ROS 2: [https://github.com/FlorisE/rospit2/blob/main/README.md ROSPIT]
* Physical integration testing for ROS 2: [https://github.com/FlorisE/rospit2/blob/main/README.md ROSPIT]
   
   


== Runtime Verification ==
=== Runtime Verification ===
* Runtime verification for Robot Operating System (ROS):  [https://github.com/autonomy-and-verification-uol/ROSMonitoring ROSMonitoring]
* Runtime verification for Robot Operating System (ROS):  [https://github.com/autonomy-and-verification-uol/ROSMonitoring ROSMonitoring]
* Runtime verification of Robotic Systems:  [https://github.com/autonomy-and-verification-uol/varanus  Varanus]
* Runtime verification of Robotic Systems:  [https://github.com/autonomy-and-verification-uol/varanus  Varanus]
* Runtime verification for Robot Operating System (ROS): [https://github.com/Formal-Systems-Laboratory/ROSRV  ROSRV]
* Runtime verification for Robot Operating System (ROS): [https://github.com/Formal-Systems-Laboratory/ROSRV  ROSRV]


== Multi-purpose verification tools ==
=== Multi-purpose verification tools ===
* [https://github.com/decyphir/breach Breach]
* [https://github.com/decyphir/breach Breach]
** How to write STL requirements
** How to write STL requirements

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

Retrieved from "https://robotistry.org/vasbok/index.php?title=Portal:Tools&oldid=75"