DMC - Revision history

David Geleßus: Update links

2021-02-04T17:20:38Z

Update links

← Older revision		Revision as of 17:20, 4 February 2021
Line 18:		Line 18:

	== Models ==		== Models ==
	We cannot make all models public, because they we provided by industrial partners from various research projects. The models that could be make available can be downloaded from [~~http~~://~~www.stups~~.hhu.de/models/parb/]		We cannot make all models public, because they we provided by industrial partners from various research projects. The models that could be make available can be downloaded from [https://www3.hhu.de/stups/models/parb/]

	== RESULTS ==		== RESULTS ==
	The results of the experiments are shown in Jens Bendisposto's dissertation. A preprint is available from [~~http~~://~~www.stups~~.uni-duesseldorf.de/w/~~Directed_and_Distributed_Model_Checking_of_B_Specifications_(Preprint)~~]		The results of the experiments are shown in Jens Bendisposto's dissertation. A preprint is available from [https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=34472]

Jens Bendisposto at 04:13, 9 April 2015

2015-04-09T04:13:13Z

← Older revision		Revision as of 04:13, 9 April 2015
Line 1:		Line 1:
	{{DISPLAYTITLE:Distributed Model Checking : Experimental evaluation}}		{{DISPLAYTITLE:Distributed Model Checking : Experimental evaluation}}
			__NOTOC__
			We used three different setups to evaluate the distributed version of ProB.

	~~This page explains~~ the ~~methodology~~ of the experiments ~~carried out~~ to ~~evaluate~~ the ~~distributed version~~ of ~~ProB~~.		* A standalone multi core computer
			* Amazon EC2 Instances
			* The HILBERT cluster


			== Multicore Computer ==
			We used a hexacore 3.33GHz Mac Pro with 16GB of RAM. On this computer we benchmarked all models regardless whether we expected them to be scalable or not. We varied the number of used cores from 1 up to 12 hyperthreads. Each experiment was repeated at least 5 times.

			== Amazon EC2 Instances ==
			We used c3.8xlarge instances, each of which has 32 virtual CPUs and is equipped with 64 GB of RAM. We used the Mac Pro to get an impression if and how well the B models scale. From the experiments, we chose those models that seemed to scale well and ran the benchmarks on the Amazon EC computer with a higher number of workers. Models that did not scale on the Mac Pro were not considered as they would not scale on more processors. We used 2 or 4 instances connected with 10 GBit ethernet connection. Each experiment was repeated at least 5 times.

			== HILBERT ==
			We used the high performance cluster at the university of Düsseldorf (HILBERT) for a single model. The model could not be cheked using a single core because it would have taken too long. Based on a partial execution, it would take about 17 days on a single core on the Mac Pro. The model was checked with different numbers of cores on the HILBERT cluster. We varied between 44 and 140 cores. On the cluster we only executed the experiments once but all experiments on the other platforms indicated that the variation between experiments could be ignored. Also the execution times of all 6 experiments seem to be consistent.

			== Models ==
			We cannot make all models public, because they we provided by industrial partners from various research projects. The models that could be make available can be downloaded from [http://www.stups.hhu.de/models/parb/]

			== RESULTS ==
			The results of the experiments are shown in Jens Bendisposto's dissertation. A preprint is available from [http://www.stups.uni-duesseldorf.de/w/Directed_and_Distributed_Model_Checking_of_B_Specifications_(Preprint)]

Jens Bendisposto at 10:41, 18 March 2015

2015-03-18T10:41:14Z

← Older revision		Revision as of 10:41, 18 March 2015
Line 1:		Line 1:
			{{DISPLAYTITLE:Distributed Model Checking : Experimental evaluation}}

	This page explains the methodology of the experiments carried out to evaluate the distributed version of ProB.		This page explains the methodology of the experiments carried out to evaluate the distributed version of ProB.

Jens Bendisposto: Created page with 'This page explains the methodology of the experiments carried out to evaluate the distributed version of ProB.'

2015-03-16T17:32:26Z

Created page with 'This page explains the methodology of the experiments carried out to evaluate the distributed version of ProB.'

New page

This page explains the methodology of the experiments carried out to evaluate the distributed version of ProB.