Difference between revisions of "Portal:Tools"

From Verification Body of Knowledge
Jump to navigation Jump to search
Line 21: Line 21:
==== Concolic Testing ====  
==== Concolic Testing ====  
Concolic testing alternates between concrete examples and symbolic analysis.   
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]





Revision as of 12:49, 28 June 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

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