Difference between revisions of "Portal:Tools"

From Verification Body of Knowledge
Jump to navigation Jump to search
 
(4 intermediate revisions by 3 users not shown)
Line 1: Line 1:
<big>Verification of Autonomous Systems -- A Selection of Tools and Processes </big>
<big>Verification of Autonomous Systems -- A Selection of Tools and Processes </big>
== 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 ==
== Tools ==
Line 6: Line 13:
* 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]]
[[Portal:Sources#Title 1|Title 1]]


=== Formal Verification ===
=== Formal Verification ===
Line 19: Line 25:
=== 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]


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"