D32 Model Animation - Revision history

imported>Tommy at 15:12, 27 January 2011

2011-01-27T15:12:55Z

← Older revision		Revision as of 15:12, 27 January 2011
Line 97:		Line 97:
	* Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation (see above).		* Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation (see above).
	* Bosch: provide animation and constraint-based deadlock detection for the Cruise Control. Indeed, proving absence of deadlocks is important to Bosch, as it means that the modelers have thought of every possible scenario. Currently, the proof obligation is so big (see above) that it is difficult to apply the provers and the feedback obtained during a failed proof attempt is not very useful. Using ProB to find concrete deadlock counterexample helps Bosch to find scenarios they have not yet thought about, and enables them to adapt the model. Once all cases have been covered, the proof of deadlock freedom can be done with Rodin's provers (at least that was the case for the smaller of the two models; the bigger one is still contains deadlocks and is being improved).		* Bosch: provide animation and constraint-based deadlock detection for the Cruise Control. Indeed, proving absence of deadlocks is important to Bosch, as it means that the modelers have thought of every possible scenario. Currently, the proof obligation is so big (see above) that it is difficult to apply the provers and the feedback obtained during a failed proof attempt is not very useful. Using ProB to find concrete deadlock counterexample helps Bosch to find scenarios they have not yet thought about, and enables them to adapt the model. Once all cases have been covered, the proof of deadlock freedom can be done with Rodin's provers (at least that was the case for the smaller of the two models; the bigger one is still contains deadlocks and is being improved).
	* SAP: provide a way to generate test cases using constraint-based animation; for more details see ~~[[D32 Model-based testing\|~~ the description of the Model-based testing work]].		* SAP: provide a way to generate test cases using constraint-based animation; for more details see the description of the Model-based testing work<ref>http://wiki.event-b.org/index.php/D32_Model-based_testing</ref>.

	= Choices / Decisions =		= Choices / Decisions =

imported>Tommy: /* Motivations */

2011-01-27T13:42:13Z

Motivations

← Older revision		Revision as of 13:42, 27 January 2011
Line 96:		Line 96:
	The above works were motivated mainly to support the following three industrial deployments:		The above works were motivated mainly to support the following three industrial deployments:
	* Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation (see above).		* Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation (see above).
	* Bosch: provide animation and constraint-based deadlock detection for the ~~Adaptive~~ Cruise Control. Indeed, proving absence of deadlocks is important to Bosch, as it means that the modelers have thought of every possible scenario. Currently, the proof obligation is so big (see above) that it is difficult to apply the provers and the feedback obtained during a failed proof attempt is not very useful. Using ProB to find concrete deadlock counterexample helps Bosch to find scenarios they have not yet thought about, and enables them to adapt the model. Once all cases have been covered, the proof of deadlock freedom can be done with Rodin's provers (at least that was the case for the smaller of the two models; the bigger one is still contains deadlocks and is being improved).		* Bosch: provide animation and constraint-based deadlock detection for the Cruise Control. Indeed, proving absence of deadlocks is important to Bosch, as it means that the modelers have thought of every possible scenario. Currently, the proof obligation is so big (see above) that it is difficult to apply the provers and the feedback obtained during a failed proof attempt is not very useful. Using ProB to find concrete deadlock counterexample helps Bosch to find scenarios they have not yet thought about, and enables them to adapt the model. Once all cases have been covered, the proof of deadlock freedom can be done with Rodin's provers (at least that was the case for the smaller of the two models; the bigger one is still contains deadlocks and is being improved).
	* SAP: provide a way to generate test cases using constraint-based animation; for more details see [[D32 Model-based testing\| the description of the Model-based testing work]].		* SAP: provide a way to generate test cases using constraint-based animation; for more details see [[D32 Model-based testing\| the description of the Model-based testing work]].

imported>Tommy: /* Constraint-Based Deadlock Checking */

2011-01-27T13:41:47Z

Constraint-Based Deadlock Checking

← Older revision		Revision as of 13:41, 27 January 2011
Line 34:		Line 34:

	== Constraint-Based Deadlock Checking ==		== Constraint-Based Deadlock Checking ==
	Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's ~~Adaptive~~ Cruise Control. We are tackling the problem of finding deadlocks via constraint solving rather than by model checking. Indeed, model checking is problematic when the out-degree is very large. In particular, quite often there can be a practically infinite number of ways to instantiate the constants of a B model. In this case, model checking will only find deadlocks for the given constants		Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's Cruise Control. We are tackling the problem of finding deadlocks via constraint solving rather than by model checking. Indeed, model checking is problematic when the out-degree is very large. In particular, quite often there can be a practically infinite number of ways to instantiate the constants of a B model. In this case, model checking will only find deadlocks for the given constants
	chosen.		chosen.

imported>Tommy: /* Siemens Data Validation */

2011-01-27T12:09:44Z

Siemens Data Validation

← Older revision		Revision as of 12:09, 27 January 2011
Line 11:		Line 11:
	* Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the São Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper <ref name="fm2009">M. Leuschel, J. Falampin, F. Fritz, D. Plagge, Automated Property Verification for Large Scale B Models, FM'2009, LNCS 5850, Springer-Verlag, 2009</ref>only contained the initial San Juan case study, which was used to evaluate the potential of our approach. In this article we describe the previous method adopted by Siemens in much more detail, as well as explaining the performance issues with Atelier B.		* Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the São Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper <ref name="fm2009">M. Leuschel, J. Falampin, F. Fritz, D. Plagge, Automated Property Verification for Large Scale B Models, FM'2009, LNCS 5850, Springer-Verlag, 2009</ref>only contained the initial San Juan case study, which was used to evaluate the potential of our approach. In this article we describe the previous method adopted by Siemens in much more detail, as well as explaining the performance issues with Atelier B.
	* Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.		* Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.
	* ~~Investigation~~ about the ongoing validation process of ProB, which is required by Siemens to allow them to use ProB instead of the existing method. The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.		* Reports about the ongoing validation process of ProB, which is required by Siemens to allow them to use ProB instead of the existing method. The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.

	Also, since <ref name="fm2009"/>, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).		Also, since <ref name="fm2009"/>, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).

imported>Tommy: /* Siemens Data Validation */

2011-01-27T12:08:39Z

Siemens Data Validation

← Older revision		Revision as of 12:08, 27 January 2011
Line 9:		Line 9:

	The most important contributions of the last 12 months are:		The most important contributions of the last 12 months are:
	* Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the São Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper <ref name="fm2009">M. Leuschel, J. Falampin, F. Fritz, D. Plagge, Automated Property Verification for Large Scale B Models, FM'2009, LNCS 5850, Springer-Verlag, 2009</ref>only contained the initial San Juan case study, which was used to evaluate the potential of our approach.		* Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the São Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper <ref name="fm2009">M. Leuschel, J. Falampin, F. Fritz, D. Plagge, Automated Property Verification for Large Scale B Models, FM'2009, LNCS 5850, Springer-Verlag, 2009</ref>only contained the initial San Juan case study, which was used to evaluate the potential of our approach. In this article we describe the previous method adopted by Siemens in much more detail, as well as explaining the performance issues with Atelier B.
	* In this article we describe the previous method adopted by Siemens in much more detail, as well as explaining the performance issues with Atelier B.
	* Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.		* Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.
	* ~~We provide more details~~ about the ongoing validation process of ProB, which is required by Siemens ~~for it~~ to use ProB ~~to replace~~ the existing method. The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.		* Investigation about the ongoing validation process of ProB, which is required by Siemens to allow them to use ProB instead of the existing method. The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.

	Also, since <ref name="fm2009"/>, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).		Also, since <ref name="fm2009"/>, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).

imported>Tommy: /* Siemens Data Validation */

2011-01-27T12:02:02Z

Siemens Data Validation

← Older revision		Revision as of 12:02, 27 January 2011
Line 4:		Line 4:

	== Siemens Data Validation ==		== Siemens Data Validation ==
	STS are successfully using the B-method and have over the years acquired considerable expertise in its application. One aspect of the current development process which is unfortunately still problematic is the validation of properties of parameters ~~only known at deployment time~~, such as the rail network topology parameters. Up to now, Siemens was using a custom version of Atelier B to check these. However, the data parameters are nowadays becoming so large (relations with thousands of tuples) that Atelier B quite often runs out of memory, even with the dedicated proof rules and with maximum memory allocated. In some of the bigger, more recent models, just substituting values for variables fails with out-of-memory conditions. ~~This means that~~ these properties ~~have to be checked by hand~~ (e.g., by creating huge spreadsheets on paper for the compatibility constraints of all possible itineraries), ~~which~~ is very costly and arguably less reliable than automated checking		STS are successfully using the B-method and have over the years acquired considerable expertise in its application. One aspect of the current development process, which is unfortunately still problematic, is the validation of properties on configuration parameters. These parameters, such as the rail network topology parameters, are only known at deployment time. Up to now, Siemens was using a custom version of Atelier B to check properties on these parameters. However, the data parameters are nowadays becoming so large (relations with thousands of tuples) that Atelier B quite often runs out of memory, even with the dedicated proof rules and with maximum memory allocated. In some of the bigger and more recent models, just substituting values for variables fails with out-of-memory conditions. The alternative consisting in the manual checking of these properties (e.g., by creating huge spreadsheets on paper for the compatibility constraints of all possible itineraries), is very costly and arguably less reliable than automated checking.

	Previously we had established the feasibility of using the ProB tool on a case study (metro of San Juan) to validate runtime data for the industrial B models, replacing a month worth of effort by a few minutes of calculation ~~with ProB~~. The next step was to apply ProB to ongoing developments of Siemens and to ~~enable~~ Siemens to use ProB in their SIL4 development chain.		Previously, we had established the feasibility of using the ProB tool on a case study (metro of San Juan) to validate runtime data for the industrial B models, replacing a month worth of effort by a few minutes of calculation. The next step was to apply ProB to ongoing developments of Siemens and to allow Siemens to use ProB in their SIL4 development chain.

	The most important contributions of the last 12 months are:		The most important contributions of the last 12 months are:

imported>Tommy: /* Siemens Data Validation */

2011-01-27T11:33:52Z

Siemens Data Validation

← Older revision		Revision as of 11:33, 27 January 2011
Line 9:		Line 9:

	The most important contributions of the last 12 months are:		The most important contributions of the last 12 months are:
	* Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the ~~S\~{a}o~~ Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper <ref name="fm2009">M. Leuschel, J. Falampin, F. Fritz, D. Plagge, Automated Property Verification for Large Scale B Models, FM'2009, LNCS 5850, Springer-Verlag, 2009</ref>only contained the initial San Juan case study, which was used to evaluate the potential of our approach.		* Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the São Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper <ref name="fm2009">M. Leuschel, J. Falampin, F. Fritz, D. Plagge, Automated Property Verification for Large Scale B Models, FM'2009, LNCS 5850, Springer-Verlag, 2009</ref>only contained the initial San Juan case study, which was used to evaluate the potential of our approach.
	* In this article we describe the previous method adopted by Siemens in much more detail, as well as explaining the performance issues with Atelier B.		* In this article we describe the previous method adopted by Siemens in much more detail, as well as explaining the performance issues with Atelier B.
	* Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.		* Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.

imported>Tommy at 13:06, 21 December 2010

2010-12-21T13:06:51Z

imported>Tommy: /* References */

2010-12-21T13:04:24Z

References

← Older revision		Revision as of 13:04, 21 December 2010
Line 121:		Line 121:
	* Further improvements in the constraint-solving kernel of ProB; in particular for relations and operators. A Kodkod translator is being developed.		* Further improvements in the constraint-solving kernel of ProB; in particular for relations and operators. A Kodkod translator is being developed.

	=== References ===		== References ==
	<references/>		<references/>

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Leuschel: /* Choices / Decisions */

2010-12-20T14:17:40Z

Choices / Decisions

← Older revision		Revision as of 14:17, 20 December 2010
Line 105:		Line 105:
	* ProB knows which parts of the axioms are theorems (and can thus be ignored; they are often added for simplifying proof but can make constraint solving more difficult)		* ProB knows which parts of the axioms are theorems (and can thus be ignored; they are often added for simplifying proof but can make constraint solving more difficult)
	* the techniques can also be applied to classical B		* the techniques can also be applied to classical B

			For record detection we decided not to use any potential "hints" provided by the records plugin, but infer the information from the axioms. In this way, the improvement can also be applied to records generated manually (as was the case in the Bosch case study) or in a classical B setting.

	= Available Documentation =		= Available Documentation =

← Older revision		Revision as of 13:06, 21 December 2010
Line 3:		Line 3:
	Most of the improvements made to model animation and model checking are related to the industrial deployment workpackages, in particular deployment within Siemens, SAP and Bosch.		Most of the improvements made to model animation and model checking are related to the industrial deployment workpackages, in particular deployment within Siemens, SAP and Bosch.

	=== Siemens Data Validation ===		== Siemens Data Validation ==
	STS are successfully using the B-method and have over the years acquired considerable expertise in its application. One aspect of the current development process which is unfortunately still problematic is the validation of properties of parameters only known at deployment time, such as the rail network topology parameters. Up to now, Siemens was using a custom version of Atelier B to check these. However, the data parameters are nowadays becoming so large (relations with thousands of tuples) that Atelier B quite often runs out of memory, even with the dedicated proof rules and with maximum memory allocated. In some of the bigger, more recent models, just substituting values for variables fails with out-of-memory conditions. This means that these properties have to be checked by hand (e.g., by creating huge spreadsheets on paper for the compatibility constraints of all possible itineraries), which is very costly and arguably less reliable than automated checking		STS are successfully using the B-method and have over the years acquired considerable expertise in its application. One aspect of the current development process which is unfortunately still problematic is the validation of properties of parameters only known at deployment time, such as the rail network topology parameters. Up to now, Siemens was using a custom version of Atelier B to check these. However, the data parameters are nowadays becoming so large (relations with thousands of tuples) that Atelier B quite often runs out of memory, even with the dedicated proof rules and with maximum memory allocated. In some of the bigger, more recent models, just substituting values for variables fails with out-of-memory conditions. This means that these properties have to be checked by hand (e.g., by creating huge spreadsheets on paper for the compatibility constraints of all possible itineraries), which is very costly and arguably less reliable than automated checking

Line 18:		Line 18:
	More details about this work can be found in the following works: <ref>M. Leuschel, J. Falampin, F. Fritz, D. Plagge, Automated Property Verification for Large Scale B Models, to appear in a special issue of FM'2009 in Formal Aspects of Computing, Springer-Verlag</ref> and <ref>Leuschel et al. Draft of Validation Report</ref>.		More details about this work can be found in the following works: <ref>M. Leuschel, J. Falampin, F. Fritz, D. Plagge, Automated Property Verification for Large Scale B Models, to appear in a special issue of FM'2009 in Formal Aspects of Computing, Springer-Verlag</ref> and <ref>Leuschel et al. Draft of Validation Report</ref>.

	=== Multi-level Animation ===		== Multi-level Animation ==

	Prior versions of ProB only supported the animation of a single refinement level. Abstract variables and predicates referring to them were ignored.		Prior versions of ProB only supported the animation of a single refinement level. Abstract variables and predicates referring to them were ignored.
Line 34:		Line 34:
	In the articles we summarized Event-B's current refinement methodology and showed for each proof obligation how the algorithm would find a counter-example. We presented empirical results and discussed how the algorithm can be combined with symmetry reduction.		In the articles we summarized Event-B's current refinement methodology and showed for each proof obligation how the algorithm would find a counter-example. We presented empirical results and discussed how the algorithm can be combined with symmetry reduction.

	=== Constraint-Based Deadlock Checking ===		== Constraint-Based Deadlock Checking ==
	Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's Adaptive Cruise Control. We are tackling the problem of finding deadlocks via constraint solving rather than by model checking. Indeed, model checking is problematic when the out-degree is very large. In particular, quite often there can be a practically infinite number of ways to instantiate the constants of a B model. In this case, model checking will only find deadlocks for the given constants		Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's Adaptive Cruise Control. We are tackling the problem of finding deadlocks via constraint solving rather than by model checking. Indeed, model checking is problematic when the out-degree is very large. In particular, quite often there can be a practically infinite number of ways to instantiate the constants of a B model. In this case, model checking will only find deadlocks for the given constants
	chosen.		chosen.
Line 55:		Line 55:
	* Counter examples are found by ProB for various versions of the model in 9-24 seconds (including loading, typechecking and deadlock PO generation; the constraint solving time is 1.03 to 12.86 seconds).		* Counter examples are found by ProB for various versions of the model in 9-24 seconds (including loading, typechecking and deadlock PO generation; the constraint solving time is 1.03 to 12.86 seconds).

	=== BMotionStudio for Industrial Models ===		== BMotionStudio for Industrial Models ==

	Previously, we presented BMotion Studio, a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization for discussing it with the domain expert. However, BMotion Studio had not yet reached the status of an Industrial strength tool due to the lack of important features known from modern editors.		Previously, we presented BMotion Studio, a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization for discussing it with the domain expert. However, BMotion Studio had not yet reached the status of an Industrial strength tool due to the lack of important features known from modern editors.
Line 67:		Line 67:
	More details can be found in <ref name="lukas_Master10">Lukas Ladenberger, Industrial Applications of BMotionStudio, Master's thesis. University of Düsseldorf. 2010</ref> and <ref>Lukas Ladenberger, Jens Bendisposto, Michael Leuschel, Visualising Event-B models with B-Motion Studio. Proceedings FMICS'2009. LNCS 5825, p.202-204. 2009.</ref>		More details can be found in <ref name="lukas_Master10">Lukas Ladenberger, Industrial Applications of BMotionStudio, Master's thesis. University of Düsseldorf. 2010</ref> and <ref>Lukas Ladenberger, Jens Bendisposto, Michael Leuschel, Visualising Event-B models with B-Motion Studio. Proceedings FMICS'2009. LNCS 5825, p.202-204. 2009.</ref>

	=== Evaluation of the ProB Constraint Solver ===		== Evaluation of the ProB Constraint Solver ==
	Various industrial applications have shown the need for improved constraint-solving capabilities (see CBC Deadlock, Test-Case Generation). In order to evaluate ProB, and detect areas for improvement, we have studied to what extent classical constraint satisfaction problems can be conveniently expressed as B predicates, and then solved by ProB. In particular, we have studied problems such as the n-Queens problem, graph colouring, graph isomorphism detection, time tabling, Sudoku, Hanoi, magic squares, Alphametic puzzles, and several more. We have then compared the performance with respect to other tools, such as the model checker TLC for TLA+, AnimB for Event-B, and Alloy.		Various industrial applications have shown the need for improved constraint-solving capabilities (see CBC Deadlock, Test-Case Generation). In order to evaluate ProB, and detect areas for improvement, we have studied to what extent classical constraint satisfaction problems can be conveniently expressed as B predicates, and then solved by ProB. In particular, we have studied problems such as the n-Queens problem, graph colouring, graph isomorphism detection, time tabling, Sudoku, Hanoi, magic squares, Alphametic puzzles, and several more. We have then compared the performance with respect to other tools, such as the model checker TLC for TLA+, AnimB for Event-B, and Alloy.

Line 73:		Line 73:
	For some other examples (in particular time-tabling) involving operators such as the relational image, the performance of ProB is still sub-optimal with respect to, e.g., Alloy; we plan to overcome this shortcoming in the future. Our long term goal is that B can not only be used to as a formal method for developing safety critical software, but also as a high-level constraint programming language.		For some other examples (in particular time-tabling) involving operators such as the relational image, the performance of ProB is still sub-optimal with respect to, e.g., Alloy; we plan to overcome this shortcoming in the future. Our long term goal is that B can not only be used to as a formal method for developing safety critical software, but also as a high-level constraint programming language.

	=== Various other improvements ===		== Various other improvements ==

	Mainly inspired by the Siemens and Bosch applications mentioned above, various improvements to the ProB kernel were undertaken.		Mainly inspired by the Siemens and Bosch applications mentioned above, various improvements to the ProB kernel were undertaken.