Verification Body of Knowledge - User contributions [en]

Portal:Tools

2022-06-28T11:16:27Z

Mfisher: /* Specification & Modelling */

<big>Verification of Autonomous Systems -- A Selection of Tools and Processes </big>

== Tools ==

=== 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] (not maintained)

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

=== Formal Verification ===
* 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]
* SMT solver for Neural Networks: [https://github.com/NeuralNetworkVerification/Marabou Marabou]
* Theorem prover for Cyber-Physical Systems: [http://www.ls.cs.cmu.edu/KeYmaeraX/ KeYmaera X]

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

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

=== Runtime Verification ===
* 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 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 ===

Portal:Glossary

2022-06-28T11:14:50Z

Mfisher:

Offer different classifications and groupings - in main page

* Verification techniques (tree?)
* Metrics (grouping)
* Application area (e.g. ML systems, for HRI, for medical robots)
* Related concepts (e.g. all the specification and requirements terms together)

Contents of each linked page:
* definitions with links to sources
* short discussion of how topic relates to verification of autonomous systems

'''''[[Template]]''''' for definition pages - please copy the markup from this page into your new definition page

;Acceptability
: exposure to loss (financial or otherwise) from a risk that an organization is willing to tolerate
;Acceptance testing
;Accountability
;Activity
: set of tasks that describe the technical effort to accomplish a process and help generate expected outcome [https://www.nasa.gov/seh/index.html NASA Systems Engineering Handbook]
;Assessment
;Assurance
;Assurance cases
;[[Autonomous System]]
: "system which has the ability to perform intended tasks based on current state, knowledge and sensing, without human intervention" [https://shop.bsigroup.com/products/robots-and-robotic-devices-guide-to-the-ethical-design-and-application-of-robots-and-robotic-systems/standard BSI 8611:2016]
;Autonomous systems design
;Autonomy
;Automation
: allocation of system functions to machines versus humans [https://www.nasa.gov/seh/index.html NASA Systems Engineering Handbook]
;Anomaly
: unexpected performance of intended function [https://www.nasa.gov/seh/index.html NASA Systems Engineering Handbook]

;Behavior verification for autonomous systems and ML systems
;Behavioral verification

;Combining V&V Techniques
;Contextual reasoning
;Correctness verification
;Credibility
;Cross-domain / multi-domain validation
;Cyber-security

;Dependability

;Executable specifications
;Experiment design
;Explainability

;Failure
: inability of a system, subsystem or component to perform its required function within specified limits [https://www.nasa.gov/seh/index.html NASA Systems Engineering Handbook]

;Failure detection and recovery
;Fault
: physical or logical cause, which explains a failure [https://www.nasa.gov/seh/index.html NASA Systems Engineering Handbook]
;Formal methods for autonomous systems
;Formal modelling
;Formal software verification
;Functional assurance
;Functional requirements
;Functional verification

;HRI (Human-robot interactions)
;HRI verification
;Hybrid Logical/Dynamical Planning and Verification

;Generalizability

;Integrity of autonomous systems

;Liability
;Licensing and certification

;Model-based evaluation

;Objective evidence
: ISO 9000:2015 - "data, supporting the existence or verity of something" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]

;Operational design domain

;Process
: "set of interrelated or interacting activities that use inputs to deliver an intended result" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]

;Qualitative assessment
;Quality requirement
: "requirement related to quality" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]
;Quality plan
: "specification of the procedures and associated resources to be applied when and by whom to a specific object" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]
;Quantitative assessment

;Performance evaluation and benchmarking
;Privacy

;Redundant robots
;Reliability
;Replicability
;Reproducibility
;Requirements
: Workspace and conditions/context of operations

;Requirement
: "need or expectation that is stated, generally implied or obligatory" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]

;Requirements development processes
;Resilience
;[[Responsibility]]
: Either (a) responsible development and deployment of robotics, see [https://shop.bsigroup.com/products/robots-and-robotic-devices-guide-to-the-ethical-design-and-application-of-robots-and-robotic-systems/standard BSI 8611:2016] or
: (b) responsible decisions by the autonomous system itself, see [https://doi.org/10.1016/j.artint.2022.103677 ethics for autonomous systems]
;Robot safety
;Robotic Systems
: Robot systems engineering
;Robustness
;Run-time verification and monitoring

;Safety
;Safety and security interaction
;Safety in HRI
: safety, system function
: verification of any function in the system including ML & non-deterministic functions
;Safety-centric HRI protocols
;Safety requirements
;Security
;Security requirements
;Simulation-based testing
;Sim-based evaluation
;Social/legal/ethical requirements
;Software testing and debugging
;Software tools for benchmarking and
;Software tools for testing
: software testing
;Specification
: "document stating requirements" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]
;Synthetic environment
: to develop high level test scenarios, drive test case development

;Test cases for verification purposes
;Testing
;Transparency
;Trust
;[[Trustworthiness]]
: Generally, [https://dictionary.cambridge.org/dictionary/english/trustworthy "able to be trusted"].
: In autonomous systems, moving beyond standard cyber-physical systems where trustworthiess is synonymous with reliability and extending this with [https://doi.org/10.1007/978-3-030-69128-8_2 beneficiality], i.e. evidence that the system is working for our benefit.

;Use-case scenario generation
;Use Case testing

;Validation:
: defines verification as "Confirmation, through the provision of objective evidence, that the requirements for a specific intended use or application have been fulfilled" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]
: further adds as "A system is able to accomplish its intended use, goals and objectives (i.e., meet stakeholder requirements) in the intended operational environment. The right system was built.” ISO/IEC/IEEE 15288:2015
;Verification:
: defines verification as "Confirmation, through the provision of objective evidence, that specified requirements have been fulfilled" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]
: further adds as "Verification is a set of activities that compare a system or system element against the required characteristics. This includes, but is not limited to specified requirements, design description and the system itself. The system was built right." ISO/IEC/IEEE 15288:2015

Portal:Glossary

2022-06-28T11:04:16Z

Mfisher:

Offer different classifications and groupings - in main page

* Verification techniques (tree?)
* Metrics (grouping)
* Application area (e.g. ML systems, for HRI, for medical robots)
* Related concepts (e.g. all the specification and requirements terms together)

Contents of each linked page:
* definitions with links to sources
* short discussion of how topic relates to verification of autonomous systems

'''''[[Template]]''''' for definition pages - please copy the markup from this page into your new definition page

;Acceptability
: exposure to loss (financial or otherwise) from a risk that an organization is willing to tolerate
;Acceptance testing
;Accountability
;Activity
: set of tasks that describe the technical effort to accomplish a process and help generate expected outcome [https://www.nasa.gov/seh/index.html NASA Systems Engineering Handbook]
;Assessment
;Assurance
;Assurance cases
;[[Autonomous System]]
: "system which has the ability to perform intended tasks based on current state, knowledge and sensing, without human intervention" [https://shop.bsigroup.com/products/robots-and-robotic-devices-guide-to-the-ethical-design-and-application-of-robots-and-robotic-systems/standard BSI 8611:2016]
;Autonomous systems design
;Autonomy
;Automation
: allocation of system functions to machines versus humans [https://www.nasa.gov/seh/index.html NASA Systems Engineering Handbook]
;Anomaly
: unexpected performance of intended function [https://www.nasa.gov/seh/index.html NASA Systems Engineering Handbook]

;Behavior verification for autonomous systems and ML systems
;Behavioral verification

;Combining V&V Techniques
;Contextual reasoning
;Correctness verification
;Credibility
;Cross-domain / multi-domain validation
;Cyber-security

;Dependability

;Executable specifications
;Experiment design
;Explainability

;Failure
: inability of a system, subsystem or component to perform its required function within specified limits [https://www.nasa.gov/seh/index.html NASA Systems Engineering Handbook]

;Failure detection and recovery
;Fault
: physical or logical cause, which explains a failure [https://www.nasa.gov/seh/index.html NASA Systems Engineering Handbook]
;Formal methods for autonomous systems
;Formal modelling
;Formal software verification
;Functional assurance
;Functional requirements
;Functional verification

;HRI (Human-robot interactions)
;HRI verification
;Hybrid Logical/Dynamical Planning and Verification

;Generalizability

;Integrity of autonomous systems

;Liability
;Licensing and certification

;Model-based evaluation

;Objective evidence
: ISO 9000:2015 - "data, supporting the existence or verity of something" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]

;Operational design domain

;Process
: "set of interrelated or interacting activities that use inputs to deliver an intended result" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]

;Qualitative assessment
;Quality requirement
: "requirement related to quality" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]
;Quality plan
: "specification of the procedures and associated resources to be applied when and by whom to a specific object" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]
;Quantitative assessment

;Performance evaluation and benchmarking
;Privacy

;Redundant robots
;Reliability
;Replicability
;Reproducibility
;Requirements
: Workspace and conditions/context of operations

;Requirement
: "need or expectation that is stated, generally implied or obligatory" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]

;Requirements development processes
;Resilience
;[[Responsibility]]
: Either (a) responsible development and deployment of robotics, see [https://shop.bsigroup.com/products/robots-and-robotic-devices-guide-to-the-ethical-design-and-application-of-robots-and-robotic-systems/standard BSI 8611:2016] or
: (b) responsible decisions by the autonomous system itself, see [https://doi.org/10.1016/j.artint.2022.103677 ethics for autonomous systems]
;Robot safety
;Robotic Systems
: Robot systems engineering
;Robustness
;Run-time verification and monitoring

;Safety
;Safety and security interaction
;Safety in HRI
: safety, system function
: verification of any function in the system including ML & non-deterministic functions
;Safety-centric HRI protocols
;Safety requirements
;Security
;Security requirements
;Simulation-based testing
;Sim-based evaluation
;Social/legal/ethical requirements
;Software testing and debugging
;Software tools for benchmarking and
;Software tools for testing
: software testing
;Specification
: "document stating requirements" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]
;Synthetic environment
: to develop high level test scenarios, drive test case development

;Test cases for verification purposes
;Testing
;Transparency
;Trust
;Trustworthiness

;Use-case scenario generation
;Use Case testing

;Validation:
: defines verification as "Confirmation, through the provision of objective evidence, that the requirements for a specific intended use or application have been fulfilled" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]
: further adds as "A system is able to accomplish its intended use, goals and objectives (i.e., meet stakeholder requirements) in the intended operational environment. The right system was built.” ISO/IEC/IEEE 15288:2015
;Verification:
: defines verification as "Confirmation, through the provision of objective evidence, that specified requirements have been fulfilled" [https://bsol.bsigroup.com/Bibliographic/BibliographicInfoData/000000000030412048 ISO 9000:2015]
: further adds as "Verification is a set of activities that compare a system or system element against the required characteristics. This includes, but is not limited to specified requirements, design description and the system itself. The system was built right." ISO/IEC/IEEE 15288:2015

Autonomous System

2022-06-14T11:57:00Z

Mfisher: /* Contextual Uses */

Table of Contents

<Top level summary, most common definition for ''autonomous system''>

== History ==
<Summary of the history of the term - how the definition has changed over time>
* Where was this first used? Who coined the term or started naming them like that?
* Was it called differently before?

== Contextual Uses ==
<Description of the different contexts this term is used in>
* E.g. ISO standards
* IEEE dictionary

=== Robotics: [https://shop.bsigroup.com/products/robots-and-robotic-devices-guide-to-the-ethical-design-and-application-of-robots-and-robotic-systems/standard BSI 8611:2016] ===

"system which has the ability to perform intended tasks based on current state, knowledge and sensing, without human intervention"

=== Robotics: [https://ieeexplore.ieee.org/browse/standards/dictionary?activeStatus=false&queryText=autonomous%20system IEEE Standards Dictionary] ===

This context draws from standards and published definitions in the physically-embodied robotics community, as distinct from the computer science community or the artificial intelligence community.

*;IEEE Standard 7001-2021
*: A system that has the capacity to make decisions itself in response to some input data or stimulus with a varying degree of human oversight or intervention depending on the system’s level of autonomy.

=== Artificial Intelligence: [https://ieeexplore.ieee.org/browse/standards/dictionary?activeStatus=false&queryText=autonomous%20system IEEE Standards Dictionary] ===

This context draws from standards and published definitions in the artificial intelligence community, as distinct from the computer science community or the physically-embodied robotics community.

*;IEEE Standard 7010-2021
*: A semi-autonomous or autonomous computer-controlled system programmed to carry out some task with or without limited human intervention capable of decision making by independent inference and successfully adapting to its context. An example is an A/IS that refers to a computer system instantiated in a product or service. ''NOTE—For the purposes of IEEE Std 7010, A/IS encompasses AI and information systems (IS).''

== Other Definitions ==
This section captures definitions of ''autonomous system'' that are used in other fields, outside the scope of this Body of Knowledge. They are included here to enable users to identify when their application area may introduce confusion.

==== Networking ====

''[https://csrc.nist.gov/glossary/term/autonomous_system Computing Security Resource Center (NIST)]''
*[https://nvlpubs.nist.gov/nistpubs/Legacy/SP/nistspecialpublication800-54.pdf NIST SP 800-54]: One or more routers under a single administration operating the same routing policy.
*[https://nvlpubs.nist.gov/nistpubs/TechnicalNotes/NIST.TN.2060.pdf NIST TN 2060]: An Autonomous System specifies a network, mostly an organization that can own or announce network addresses to the Internet.

Portal:People

2022-05-04T07:14:15Z

Mfisher:

== Organizations & Large Projects ==

* [https://verifiability.org/ (UK) Trustworthy Autonomous Systems: Verifiability Node]

* [https://resilience.tas.ac.uk/ (UK) Trustworthy Autonomous Systems: Resilience Node]

* [https://tas-security.lancs.ac.uk/ (UK) Trustworthy Autonomous Systems: Security Node]

* [https://trust.tas.ac.uk/ (UK) Trustworthy Autonomous Systems: Trust Node]

* [https://www.tas.org/ (UK) Trustworthy Autonomous Systems: Hub]

* [https://www.york.ac.uk/assuring-autonomy/ (UK) Assuring Autonomy International Programme]

== Research Groups ==

Organize by research focus?
Assign individual glossary pages to individual experts - people should contact the person responsible for that page instead of listing them here? Is this even a good category to have here?

== Agencies ==

Organize by ... interest? domain? (e.g. US Department of Transportation evaluation of autonomous cars group)

Portal:Glossary

2022-05-04T07:04:53Z

Mfisher:

Offer different classifications and groupings - in main page

* Verification techniques (tree?)
* Metrics (grouping)
* Application area (e.g. ML systems, for HRI, for medical robots)

Contents of each linked page:
* definitions with links to sources
* short discussion of how topic relates to verification of autonomous systems

;Acceptability
;Acceptance testing
;Accountability
;Assessment
;Assurance
;Assurance cases
;Autonomous System: "system which has the ability to perform intended tasks based on current state, knowledge and sensing, without human intervention" [https://shop.bsigroup.com/products/robots-and-robotic-devices-guide-to-the-ethical-design-and-application-of-robots-and-robotic-systems/standard BSI 8611:2016]
;Autonomous systems design
;Autonomy

;Behavior verification for autonomous systems and ML systems
;Behavioral verification

;Combining V&V Techniques
;Contextual reasoning
;Correctness verification
;Credibility
;Cross-domain / multi-domain validation
;Cyber-security

;Dependability

;Executable specifications
;Experiment design
;Explainability

;Failure detection and recovery
;Formal methods for autonomous systems
;Formal modelling
;Formal software verification
;Functional assurance
;Functional requirements
;Functional verification

;HRI (Human-robot interactions)
;HRI verification
;Hybrid Logical/Dynamical Planning and Verification

;Generalizability

;Integrity of autonomous systems

;Liability
;Licensing and certification

;Model-based evaluation

;Operational design domain

;Qualitative assessment
;Quantitative assessment

;Performance evaluation and benchmarking
;Privacy

;Redundant robots
;Reliability
;Replicability
;Reproducibility
;Requirements
: Workspace and conditions/context of operations
;Requirements development processes
;Resilience
;Responsibility
;Robot safety
;Robotic Systems
: Robot systems engineering
;Robustness
;Run-time verification and monitoring

;Safety
;Safety and security interaction
;Safety in HRI
: safety, system function
: verification of any function in the system including ML & non-deterministic functions
;Safety-centric HRI protocols
;Safety requirements
;Security
;Security requirements
;Simulation-based testing
;Sim-based evaluation
;Social/legal/ethical requirements
;Software testing and debugging
;Software tools for benchmarking and
;Software tools for testing
: software testing
;Specifications
;Synthetic environment
: to develop high level test scenarios, drive test case development

;Test cases for verification purposes
;Testing
;Transparency
;Trust
;Trustworthiness

;Use-case scenario generation
;Use Case testing

;Validation
;Verification

Portal:Tools

2022-03-22T15:15:45Z

Mfisher: /* Formal Verification */

<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 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]
* SMT solver for Neural Networks: [https://github.com/NeuralNetworkVerification/Marabou Marabou]
* Theorem prover for Cyber-Physical Systems: [http://www.ls.cs.cmu.edu/KeYmaeraX/ KeYmaera X]

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

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

== Runtime Verification ==
* 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 for Robot Operating System (ROS): [https://github.com/Formal-Systems-Laboratory/ROSRV ROSRV]

== ==

Portal:Tools

2022-03-22T15:11:26Z

Mfisher: 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..."

<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 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]
* SMT solver for Neural Networks: [https://github.com/NeuralNetworkVerification/Marabou Marabou]
* Theorem prover for Hybrid Systems: [http://www.ls.cs.cmu.edu/KeYmaeraX/ KeYmaera X]

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

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

== Runtime Verification ==
* 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 for Robot Operating System (ROS): [https://github.com/Formal-Systems-Laboratory/ROSRV ROSRV]

== ==