Difference between revisions of "Portal:Tools"

From Verification Body of Knowledge
Jump to navigation Jump to search
 
(14 intermediate revisions by 4 users not shown)
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 ==
== 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 [https://www.it.uu.se/research/group/darts/uppaal/index.shtml link], the tool C2E2 [https://publish.illinois.edu/c2e2-tool/ link], and tools mentioned in the Assured Autonomy compendium [https://assured-autonomy.org/tools 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:  [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]
* 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] (not maintained)


[[Portal:Sources#Title 1|Title 1]]


== 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 13: Line 23:
* 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 ====
Concolic testing alternates between concrete examples and symbolic analysis. 
* 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 ===
* [https://github.com/decyphir/breach Breach]
** How to write STL requirements
** Falsification of STL requirements
** Monitoring for STL formulae
** Interfacing with Simulink models using the toolbox
** Available in Github
* [https://sites.google.com/a/asu.edu/s-taliro/s-taliro S-Taliro]
** Verification
** Conformance testing
** MATLAB toolbox
* [https://gitlab.com/sbtg/psy-taliro PSY-Taliro]
** Python toolbox for S-Taliro
** Available on Gitlab
** [https://link.springer.com/chapter/10.1007/978-3-030-85248-1_15 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


== ==
=== Specifications ===
=== Formal methods ===
=== Assurance cases ===
=== Testing ===

Latest revision as of 06:15, 23 September 2022

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

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.


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

  • 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

Specifications

Formal methods

Assurance cases

Testing

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