Portal:Tools - Revision history

Arinajed at 06:15, 23 September 2022

2022-09-23T06:15:59Z

← Older revision		Revision as of 06:15, 23 September 2022
Line 5:		Line 5:
	* 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.		* 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		* 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.

Arinajed at 15:17, 19 September 2022

2022-09-19T15:17:41Z

← Older revision		Revision as of 15:17, 19 September 2022
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


	== Tools ==		== Tools ==

Signe at 12:49, 28 June 2022

2022-06-28T12:49:41Z

← Older revision		Revision as of 12:49, 28 June 2022
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]

Signe at 12:49, 28 June 2022

2022-06-28T12:49:26Z

← Older revision		Revision as of 12:49, 28 June 2022
Line 18:		Line 18:
	=== 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 for Deep Neural Networks: [https://github.com/xiaoweih/DeepConcolic DeepConcolic]
			==== Concolic Testing ====
			Concolic testing alternates between concrete examples and symbolic analysis.

			Concolic testing for Deep Neural Networks: [https://github.com/xiaoweih/DeepConcolic DeepConcolic]

Mfisher: /* Specification & Modelling */

2022-06-28T11:16:27Z

Specification & Modelling

← Older revision		Revision as of 11:16, 28 June 2022
Line 6:		Line 6:
	* 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 ===

Arinajed at 12:28, 31 May 2022

2022-05-31T12:28:48Z

@@ Line 48: / Line 48: @@
 ** Available on Gitlab
 ** [https://link.springer.com/chapter/10.1007/978-3-030-85248-1_15 Paper reference]
 == Processes ==

Arinajed at 12:26, 31 May 2022

2022-05-31T12:26:34Z

Arinajed at 12:26, 31 May 2022

2022-05-31T12:26:03Z

← Older revision		Revision as of 12:26, 31 May 2022
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 ==		== 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]
Line 46:		Line 48:
	** Available on Gitlab		** Available on Gitlab
	** [https://link.springer.com/chapter/10.1007/978-3-030-85248-1_15 Paper reference]		** [https://link.springer.com/chapter/10.1007/978-3-030-85248-1_15 Paper reference]

			== Processes ==

Signe at 12:16, 17 May 2022

2022-05-17T12:16:37Z

← Older revision		Revision as of 12:16, 17 May 2022
Line 6:		Line 6:
	* 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]

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

AIDejanira at 12:52, 5 April 2022

2022-04-05T12:52:03Z

← Older revision		Revision as of 12:52, 5 April 2022
Line 42:		Line 42:
	** MATLAB toolbox		** MATLAB toolbox

	* [https://~~link.springer~~.com/~~chapter/10.1007~~/~~978-3-030-85248~~-~~1_15~~ PSY-Taliro]		* [https://gitlab.com/sbtg/psy-taliro PSY-Taliro]
	** Python toolbox for S-Taliro		** Python toolbox for S-Taliro
	** Available on ~~Github~~		** Available on Gitlab
			** [https://link.springer.com/chapter/10.1007/978-3-030-85248-1_15 Paper reference]

← Older revision		Revision as of 12:26, 31 May 2022
Line 11:		Line 11:


	== 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 17:		Line 17:
	* 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 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 ==		=== Multi-purpose verification tools ===
	* [https://github.com/decyphir/breach Breach]		* [https://github.com/decyphir/breach Breach]
	** How to write STL requirements		** How to write STL requirements