Difference between revisions of "Portal:Tools"
Jump to navigation
Jump to search
(Created page with "<big>Verification of Autonomous Systems -- A Selection of Tools</big> == Specification & Modelling == * 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] * Executable Agent Specifications: [https://www.csc.liv.ac.uk/~michael/TLBook/MetateM-System/ Concurrent MetateM] == Formal Verification == * Program model-checking of age...") |
|||
| Line 11: | Line 11: | ||
* Robustness analyzer for Neural Networks: [https://github.com/eth-sri/eran ERAN] | * Robustness analyzer for Neural Networks: [https://github.com/eth-sri/eran ERAN] | ||
* SMT solver for Neural Networks: [https://github.com/NeuralNetworkVerification/Marabou Marabou] | * SMT solver for Neural Networks: [https://github.com/NeuralNetworkVerification/Marabou Marabou] | ||
* Theorem prover for | * Theorem prover for Cyber-Physical Systems: [http://www.ls.cs.cmu.edu/KeYmaeraX/ KeYmaera X] | ||
== Software Testing == | == Software Testing == | ||
Revision as of 15:15, 22 March 2022
Verification of Autonomous Systems -- A Selection of Tools
Specification & Modelling
- Modelling of Robotic Systems: RoboTool
- Modelling of Robotic Systems: GenoM
- Executable Agent Specifications: Concurrent MetateM
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