D23 ProB - Revision history

imported>Pascal: /* For PDF rendering */

2010-01-28T15:55:11Z

For PDF rendering

← Older revision		Revision as of 15:55, 28 January 2010
Line 21:		Line 21:
	= Motivations =		= Motivations =

	=== Multi-level Animation and Validation ===		== Multi-level Animation and Validation ==

	Thus far ProB only allowed single-level animation, i.e. the animator would animate a single refinement level in isolation.		Thus far ProB only allowed single-level animation, i.e. the animator would animate a single refinement level in isolation.
Line 35:		Line 35:
	The new algorithm has been successfully applied to various case studies, and thus far up to 14 levels have been animated concurrently without problem.		The new algorithm has been successfully applied to various case studies, and thus far up to 14 levels have been animated concurrently without problem.

	=== B-Motion Studio ===		== B-Motion Studio ==

	It is often very important to be able to show a formal model to a domain expert or manager, not versed in formal methods.		It is often very important to be able to show a formal model to a domain expert or manager, not versed in formal methods.
Line 44:		Line 44:
	To run a graphical visualisation, the ProB animator is used.		To run a graphical visualisation, the ProB animator is used.

	=== Test-Case Generation ===		== Test-Case Generation ==

	During deployment in the SAP workpackage it became clear that test-case generation from the Event-B models is required for success.		During deployment in the SAP workpackage it became clear that test-case generation from the Event-B models is required for success.
Line 50:		Line 50:
	Optimisations, to reduce the length and number of test cases, as well as to minimise race conditions, have been implemented.		Optimisations, to reduce the length and number of test cases, as well as to minimise race conditions, have been implemented.

	=== Scalability, Application by Siemens and Validation ===		== Scalability, Application by Siemens and Validation ==
	We tackled a case study in WP2, which centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes).		We tackled a case study in WP2, which centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes).

Line 61:		Line 61:
	This leads to the next task: the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens.		This leads to the next task: the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens.

	=== Proof Directed Model Checking ===		== Proof Directed Model Checking ==

	In order to improve the performance and scalability of animation and model checking with ProB, we want to make use of the proof information available in an integrated platform such as Rodin.		In order to improve the performance and scalability of animation and model checking with ProB, we want to make use of the proof information available in an integrated platform such as Rodin.
Line 68:		Line 68:
	Our first implementation has shown significant reduction of the model checking effort for industrial applications. It uses proof information obtained from Rodin to remove invariants that are proven to hold. Actually, if unproven(e) is the unproven part of the invariant for event e, and a state is reachable via events e and f, we only need to check the intersection of unproven(e) and unproven(f) (see [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=253 Jens Bendisposto, Michael Leuschel. Proof Assisted Model Checking for B. ICFEM 2009.]).		Our first implementation has shown significant reduction of the model checking effort for industrial applications. It uses proof information obtained from Rodin to remove invariants that are proven to hold. Actually, if unproven(e) is the unproven part of the invariant for event e, and a state is reachable via events e and f, we only need to check the intersection of unproven(e) and unproven(f) (see [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=253 Jens Bendisposto, Michael Leuschel. Proof Assisted Model Checking for B. ICFEM 2009.]).

	=== SAT/SMT/Kodkod ===		== SAT/SMT/Kodkod ==

	In this subtask we investigate alternate approaches to validate high-level B models using techniques and tools based on BDDs, SAT-solving and SMT-solving.		In this subtask we investigate alternate approaches to validate high-level B models using techniques and tools based on BDDs, SAT-solving and SMT-solving.
Line 76:		Line 76:
	When looking for constants that satisfy the axioms or when trying to find counterexamples for proof obligations (see next Disprover paragraph), SAT resp. SMT solving techniques look very promising to support ProB's constraint solving approach.		When looking for constants that satisfy the axioms or when trying to find counterexamples for proof obligations (see next Disprover paragraph), SAT resp. SMT solving techniques look very promising to support ProB's constraint solving approach.

	=== Disprover ===		== Disprover ==

	In order to help the user, we wanted to make it possible to apply ProB to individual proof obligations.		In order to help the user, we wanted to make it possible to apply ProB to individual proof obligations.
Line 151:		Line 151:
	In future, it is planned to work on the following topics:		In future, it is planned to work on the following topics:

	=== Model-based Testing ===		== Model-based Testing ==

	* Directed model checking to achieve coverage (DEPLOY extension; flow graphs).		* Directed model checking to achieve coverage (DEPLOY extension; flow graphs).
Line 159:		Line 159:
	* Move from prototype to real product.		* Move from prototype to real product.

	=== B-Motion Studio ===		== B-Motion Studio ==

	* Experiment with existing Flash animation and B model of ClearSy.		* Experiment with existing Flash animation and B model of ClearSy.
	* Improve usability, more widgets.		* Improve usability, more widgets.

	=== Validation of ProB ===		== Validation of ProB ==

	* Test coverage analysis for Prolog code.		* Test coverage analysis for Prolog code.
	* Validation document to be delivered to Siemens.		* Validation document to be delivered to Siemens.

	=== Scalability ===		== Scalability ==

	* More experiments with SAT, SMT, BDD techniques.		* More experiments with SAT, SMT, BDD techniques.
Line 177:		Line 177:
	* Adaption of ProB for the upcoming mathematical extensions. Indeed, for the moment the Rodin user is often required to model basic datatypes (records, sequences,...) or operators (transitive closure) herself. This is a big challenge to the animator, which does not know that the constants and variables of the machine (e.g. injective functions) are "simply" meant to model quite basic datatypes. With the introduction of mathematical extensions for records, transitive closure, ... this hurdle will be overcome.		* Adaption of ProB for the upcoming mathematical extensions. Indeed, for the moment the Rodin user is often required to model basic datatypes (records, sequences,...) or operators (transitive closure) herself. This is a big challenge to the animator, which does not know that the constants and variables of the machine (e.g. injective functions) are "simply" meant to model quite basic datatypes. With the introduction of mathematical extensions for records, transitive closure, ... this hurdle will be overcome.

	=== Usability ===		== Usability ==
	* Feedback errors found by ProB into the PO view (as red icons).		* Feedback errors found by ProB into the PO view (as red icons).
	* Improve disprover, detect when it is a decision procedure.		* Improve disprover, detect when it is a decision procedure.

imported>Pascal: D23 PRO-B moved to D23 ProB

2010-01-26T16:00:48Z

D23 PRO-B moved to D23 ProB

← Older revision	Revision as of 16:00, 26 January 2010
(No difference)

imported>Pascal: /* Planning */

2010-01-26T16:00:03Z

Planning

← Older revision		Revision as of 16:00, 26 January 2010
Line 149:		Line 149:

	= Planning =		= Planning =
			In future, it is planned to work on the following topics:

	=== Model-based Testing ===		=== Model-based Testing ===

imported>Tommy: /* Scalability, Application by Siemens and Validation */

2009-12-10T17:07:26Z

Scalability, Application by Siemens and Validation

← Older revision		Revision as of 17:07, 10 December 2009
Line 51:		Line 51:

	=== Scalability, Application by Siemens and Validation ===		=== Scalability, Application by Siemens and Validation ===
	We tackled a case study in WP2, which centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes). I		We tackled a case study in WP2, which centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes).

	The motivation then was to try and use ProB for this task.		The motivation then was to try and use ProB for this task.

imported>Pascal: /* Usability */

2009-12-07T18:07:05Z

Usability

← Older revision		Revision as of 18:07, 7 December 2009
Line 181:		Line 181:
	* Allow the user to easier inspect elements of the animated model: the cause of errors, why events are not enabled, etc.		* Allow the user to easier inspect elements of the animated model: the cause of errors, why events are not enabled, etc.
	* Further improvements to the GUI: 2-D Viewer, better multi-level animation view.		* Further improvements to the GUI: 2-D Viewer, better multi-level animation view.

			[[Category:D23 Deliverable]]

imported>Pascal: /* Typo */

2009-12-04T10:51:34Z

Typo

← Older revision		Revision as of 10:51, 4 December 2009
Line 152:		Line 152:
	=== Model-based Testing ===		=== Model-based Testing ===

	* Directed model checking to achieve coverage (~~Deploy~~ extension; flow graphs).		* Directed model checking to achieve coverage (DEPLOY extension; flow graphs).
	* Integrate algorithm into Rodin.		* Integrate algorithm into Rodin.
	* Make algorithm more generic.		* Make algorithm more generic.

imported>Pascal: /* Published Papers */

2009-12-04T10:38:26Z

Published Papers

← Older revision		Revision as of 10:38, 4 December 2009
Line 141:		Line 141:

	[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=257 Edd Turner, Michael Butler, Michael Leuschel. A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. ABZ'2010.]		[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=257 Edd Turner, Michael Butler, Michael Leuschel. A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. ABZ'2010.]


	=== B-Motion Studio ===		=== B-Motion Studio ===

imported>Pascal: /* Typos */

2009-12-04T10:37:53Z

Typos

← Older revision		Revision as of 10:37, 4 December 2009
Line 103:		Line 103:
	=== Improved Kernel to deal with large sets and relations ===		=== Improved Kernel to deal with large sets and relations ===
	In this part we describe the successful application of the ProB validation tool on an industrial case study. The case study centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes). In this paper we show how we were able to use ProB to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in around 17 minutes that were manually uncovered in about one man-month. This achievement required the extension of the ProB kernel for large sets as well as an improved constraint propagation phase. We also outline some of the effort and features that were required in moving from a tool capable of dealing with medium-sized examples towards a tool able to deal with actual industrial specifications. Notably, a new parser and type checker had to be developed. We also touch upon the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens		In this part we describe the successful application of the ProB validation tool on an industrial case study. The case study centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes). In this paper we show how we were able to use ProB to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in around 17 minutes that were manually uncovered in about one man-month. This achievement required the extension of the ProB kernel for large sets as well as an improved constraint propagation phase. We also outline some of the effort and features that were required in moving from a tool capable of dealing with medium-sized examples towards a tool able to deal with actual industrial specifications. Notably, a new parser and type checker had to be developed. We also touch upon the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens


	[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=248 Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge. Automated Property Verification for Large Scale B Models, FM'2009.]		[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=248 Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge. Automated Property Verification for Large Scale B Models, FM'2009.]
Line 116:		Line 115:
	See also [http://www.springerlink.com/content/282p2316x7165588/ Stefan Hallerstede, Michael Leuschel. How to Explain Mistakes. TFM'09.]		See also [http://www.springerlink.com/content/282p2316x7165588/ Stefan Hallerstede, Michael Leuschel. How to Explain Mistakes. TFM'09.]

	=== Test-Case Generation ===		=== Test Case Generation ===
	Choreography models describe the communication protocols between services. Testing of service choreographies is an important task for the quality assurance of service-based systems as used e.g. in the context of service-oriented architectures (SOA). The formal ~~modeling~~ of service choreographies enables a model-based integration testing (MBIT) approach. We present MBIT methods for our service choreography modeling approach called Message Choreography Models (MCM). For the model-based testing of service choreographies, MCMs are translated into Event-B models and used as input for our test generator which uses the model checker ProB.		Choreography models describe the communication protocols between services. Testing of service choreographies is an important task for the quality assurance of service-based systems as used e.g. in the context of service-oriented architectures (SOA). The formal modelling of service choreographies enables a model-based integration testing (MBIT) approach. We present MBIT methods for our service choreography modeling approach called Message Choreography Models (MCM). For the model-based testing of service choreographies, MCMs are translated into Event-B models and used as input for our test generator which uses the model checker ProB.

	[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=252 Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. Applying Model Checking to Generate Model-based Integration Tests from Choreography Models. TESTCOM/FATES 2009.]		[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=252 Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. Applying Model Checking to Generate Model-based Integration Tests from Choreography Models. TESTCOM/FATES 2009.]


	=== Proof-Directed Model Checking ===		=== Proof-Directed Model Checking ===
	With the aid of the ProB ~~Plugin~~, the Rodin Platform provides an integrated environment for editing, proving, animating and model checking Event-B models. This is of considerable benefit to the ~~modeler~~, as it allows him to switch between the various tools to validate, debug and improve his or her models. The crucial idea of this paper is that the integrated platform also provides benefits to the tool developer, i.e., it allows easy access to information from other tools. Indeed, there has been considerable interest in combining model checking, proving and testing. In previous work we have already shown how a model checker can be used to complement the Event-B proving environment, by acting as a disprover. In this paper we show how the prover can help improve the efficiency of the animator and model checker.		With the aid of the ProB plug-in, the Rodin Platform provides an integrated environment for editing, proving, animating and model checking Event-B models. This is of considerable benefit to the modeller, as it allows him to switch between the various tools to validate, debug and improve his or her models. The crucial idea of this paper is that the integrated platform also provides benefits to the tool developer, i.e. it allows easy access to information from other tools. Indeed, there has been considerable interest in combining model checking, proving and testing. In previous work we have already shown how a model checker can be used to complement the Event-B proving environment, by acting as a disprover. In this paper we show how the prover can help to improve the efficiency of the animator and model checker.

	[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=253 Jens Bendisposto, Michael Leuschel. Proof Assisted Model Checking for B. ICFEM 2009.]		[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=253 Jens Bendisposto, Michael Leuschel. Proof Assisted Model Checking for B. ICFEM 2009.]

	=== Debugging Tricky Proof Obligations with the ProB Disprover ===		=== Debugging Tricky Proof Obligations with the ProB Disprover ===
	While a large number of proof obligations can be discharged automatically by tools such as the ~~RODIN~~ platform, a considerable number still have to be proven interactively. In this paper, we we describe a disprover ~~plugin~~ for ~~RODIN~~ that utilizes ProB to automatically find counterexamples for a given problematic proof obligation. In case the disprover finds a counterexample, the user can directly investigate the source of ~~teh~~ problem, as pinpointed by the counterexample. We also discuss under which circumstances our plug-in can be used as a prover, i.e., when the absence of a counterexample		While a large number of proof obligations can be discharged automatically by tools such as the Rodin platform, a considerable number still have to be proven interactively. In this paper, we describe a disprover plug-in for Rodin that utilizes ProB to automatically find counterexamples for a given problematic proof obligation. In case the disprover finds a counterexample, the user can directly investigate the source of the problem, as pinpointed by the counterexample. We also discuss under which circumstances our plug-in can be used as a prover, i.e. when the absence of a counterexample actually is a proof of the proof obligation.
	actually is a proof of the proof obligation.

	[http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 Olivier Ligot, Jens Bendisposto, Michael Leuschel. Debugging Event-B Models using the ProB Disprover Plug-in. AFADL 2007.]		[http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 Olivier Ligot, Jens Bendisposto, Michael Leuschel. Debugging Event-B Models using the ProB Disprover Plug-in. AFADL 2007.]
Line 141:		Line 138:
	=== Validation of ProB ===		=== Validation of ProB ===

	Symmetry reduction is a model checking technique that can help alleviate the problem of state space explosion, by preventing redundant state space exploration. In previous work, we have developed three effective approaches to symmetry reduction for B that have been implemented into the ProB model checker, and we have proved the soundness of our state symmetries. However, it is also important to show our techniques are sound with respect to standard model checking, at the algorithmic level. In this paper, we present a retrospective B development that addresses this issue through a series of B refinements. This work also demonstrates the valuable insights into a system that can be gained through formal modelling.		Symmetry reduction is a model checking technique that can help to alleviate the problem of state space explosion, by preventing redundant state space exploration. In previous work, we have developed three effective approaches to symmetry reduction for B that have been implemented into the ProB model checker, and we have proved the soundness of our state symmetries. However, it is also important to show that our techniques are sound with respect to standard model checking, at the algorithmic level. In this paper, we present a retrospective B development that addresses this issue through a series of B refinements. This work also demonstrates the valuable insights into a system that can be gained through formal modelling.

	[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=257 Edd Turner, Michael Butler, Michael Leuschel. A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. ABZ'2010.]		[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=257 Edd Turner, Michael Butler, Michael Leuschel. A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. ABZ'2010.]
Line 153:		Line 150:

	= Planning =		= Planning =
	~~This paragraph shall give a timeline and current status (as of 29 Jan 2010).~~

	=== Model-based Testing ===		=== Model-based Testing ===

	* Directed ~~Model Checking~~ to achieve coverage (Deploy extension; ~~Flow Graphs~~)		* Directed model checking to achieve coverage (Deploy extension; flow graphs).
	* Integrate ~~Algorithm~~ into Rodin		* Integrate algorithm into Rodin.
	* Make ~~Algorithm~~ more generic		* Make algorithm more generic.
	* Top-down multi-level animation		* Top-down multi-level animation.
	* Move from prototype to real product		* Move from prototype to real product.

	=== B-Motion Studio ===		=== B-Motion Studio ===

	* Experiment with existing Flash animation and B model of ClearSy		* Experiment with existing Flash animation and B model of ClearSy.
	* Improve usability, more widgets		* Improve usability, more widgets.

	=== Validation of ProB ===		=== Validation of ProB ===

	* Test coverage analysis for Prolog code		* Test coverage analysis for Prolog code.
	* Validation ~~Document~~ to be delivered to Siemens		* Validation document to be delivered to Siemens.

	=== Scalability ===		=== Scalability ===

	* More experiments with SAT, SMT, BDD techniques		* More experiments with SAT, SMT, BDD techniques.

	* Integration of Kodkod into ProB ~~for solving~~ complicated predicates over first order relations and simple sets		* Integration of Kodkod into ProB to solve complicated predicates over first order relations and simple sets.

	* Adaption of ProB for the upcoming mathematical extensions. Indeed, for the moment the Rodin user is often required to model basic datatypes (records, sequences,...) or operators (transitive closure) herself. This is a big challenge to the animator, which does not know that the constants and variables of the machine (e.g., injective functions) are "simply" meant to model quite basic datatypes. With the introduction of mathematical extensions for records, transitive closure, ... this hurdle will be overcome.		* Adaption of ProB for the upcoming mathematical extensions. Indeed, for the moment the Rodin user is often required to model basic datatypes (records, sequences,...) or operators (transitive closure) herself. This is a big challenge to the animator, which does not know that the constants and variables of the machine (e.g. injective functions) are "simply" meant to model quite basic datatypes. With the introduction of mathematical extensions for records, transitive closure, ... this hurdle will be overcome.

	=== Usability ===		=== Usability ===
	* Feedback errors found by ProB into the PO view (as red icons)		* Feedback errors found by ProB into the PO view (as red icons).
	* Improve ~~Disprover~~, detect when it is a decision procedure		* Improve disprover, detect when it is a decision procedure.
	* Allow the user to easier inspect elements of the animated model: the cause of errors, why events are not enabled, etc.		* Allow the user to easier inspect elements of the animated model: the cause of errors, why events are not enabled, etc.
	* Further improvements to GUI: 2-D Viewer, better multi-level animation view		* Further improvements to the GUI: 2-D Viewer, better multi-level animation view.

imported>Pascal: /* Motivations */

2009-12-04T10:28:31Z

Motivations

← Older revision		Revision as of 10:28, 4 December 2009
Line 20:		Line 20:

	= Motivations =		= Motivations =
	This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.


	=== Multi-level Animation and Validation ===		=== Multi-level Animation and Validation ===

	Thus far ProB only ~~alllowed~~ single-level animation, i.e., the animator would animate a single refinement level in isolation.		Thus far ProB only allowed single-level animation, i.e. the animator would animate a single refinement level in isolation.
	This meant that ProB was not able to detect a large class of potential errors in the model:		This meant that ProB was not able to detect a large class of potential errors in the model:
	* a broken gluing invariant		* A broken gluing invariant.
	* an invalid witness		* An invalid witness.
	* ~~violation~~ of guard strengthening		* Violation of guard strengthening.
	* ~~violation~~ of variant decrease (resp. decrease or stability) for convergent (resp. anticipated) events		* Violation of variant decrease (resp. decrease or stability) for convergent (resp. anticipated) events.

	The new validation algorithm now can animate a range of refinements together. The user can decide which levels are to be animated together.		The new validation algorithm now can animate a range of refinements together. The user can decide which levels are to be animated together.
	As such, all of the above errors can now be detected by ProB.		As such, all of the above errors can now be detected by ProB.
	User experience is also improved, as he or she can inspect also the abstract variables.		User experience is also improved, as he or she can inspect also the abstract variables.
	The new algorithm has been ~~sucessfully~~ applied to various case studies, and thus far up to 14 levels have been animated concurrently without problem.		The new algorithm has been successfully applied to various case studies, and thus far up to 14 levels have been animated concurrently without problem.


	=== B-Motion Studio ===		=== B-Motion Studio ===
Line 49:		Line 46:
	=== Test-Case Generation ===		=== Test-Case Generation ===

	During deployment in the SAP workpackage it became clear that test-case generation from the Event-B models		During deployment in the SAP workpackage it became clear that test-case generation from the Event-B models is required for success.
	is required for success.
	In this task, we have developed a first algorithm for test-case generation, which ensures complete transition coverage of a high-level model, and translates the test-cases into traces of a refined model, so that the tests can be run on the "real" system.		In this task, we have developed a first algorithm for test-case generation, which ensures complete transition coverage of a high-level model, and translates the test-cases into traces of a refined model, so that the tests can be run on the "real" system.
	Optimisations, to reduce the length and number of test cases, as well as to minimise race conditions, have been implemented.		Optimisations, to reduce the length and number of test cases, as well as to minimise race conditions, have been implemented.

	=== Scalability, Application by Siemens and Validation ===		=== Scalability, Application by Siemens and Validation ===
	We tackled a case study in WP2, which centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes). I		We tackled a case study in WP2, which centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes). I

	The motivation then was to try and use ProB for this task.		The motivation then was to try and use ProB for this task.
Line 61:		Line 57:
	The ProB parser and type checker also had to be re-developed to be able to deal with large industrial specifications.		The ProB parser and type checker also had to be re-developed to be able to deal with large industrial specifications.

	The case study was a ~~succcess~~:ProB was able to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in around 17 minutes that were manually uncovered in about one man-month.		The case study was a success: ProB was able to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in around 17 minutes that were manually uncovered in about one man-month.

	This leads to the next task: the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens		This leads to the next task: the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens.

	=== Proof Directed Model Checking ===		=== Proof Directed Model Checking ===
Line 74:		Line 70:
	=== SAT/SMT/Kodkod ===		=== SAT/SMT/Kodkod ===

	In this subtask we investigate alternate approaches ~~for validating~~ high-level B models using techniques and tools based on BDDs, SAT-solving and SMT-solving.		In this subtask we investigate alternate approaches to validate high-level B models using techniques and tools based on BDDs, SAT-solving and SMT-solving.
	The overall motivation is to improve the scalability of the animator and model checker.		The overall motivation is to improve the scalability of the animator and model checker.

	When searching for variable values that satisfy a certain predicate,		When searching for variable values that satisfy a certain predicate, experience showed that ProB performs best when some values are already known, as in finding state transitions where all values of the previous state are known.
	experience showed that ProB performs best when some values are already known,		When looking for constants that satisfy the axioms or when trying to find counterexamples for proof obligations (see next Disprover paragraph), SAT resp. SMT solving techniques look very promising to support ProB's constraint solving approach.
	as in finding state transitions where all values of the previous state are known.
	When looking for constants that satisfy the axioms or when trying to find counterexamples for proof obligations (see next Disprover paragraph),
	SAT resp. SMT solving techniques look very promising to support ProB's constraint solving approach.

	=== Disprover ===		=== Disprover ===
Line 87:		Line 80:
	In order to help the user, we wanted to make it possible to apply ProB to individual proof obligations.		In order to help the user, we wanted to make it possible to apply ProB to individual proof obligations.
	In some cases, this enables proving a sequent by exhaustive case analysis.		In some cases, this enables proving a sequent by exhaustive case analysis.
	Also, if ProB finds a ~~counter example~~, the user gets important feedback: the proof obligation cannot be discharged, along with a reason why.		Also, if ProB finds a counterexample, the user gets important feedback: the proof obligation cannot be discharged, along with a reason why.

	= Choices / Decisions =		= Choices / Decisions =

imported>Pascal: /* Overview */

2009-12-04T10:22:19Z

Overview

← Older revision		Revision as of 10:22, 4 December 2009
Line 1:		Line 1:
	= Overview =		= Overview =
	This part of the deliverable describes ~~improvement~~ of the ProB animation and model checking ~~plugin~~.		This part of the deliverable describes improvements of the ProB animation and model checking plug-in.

	The improvements and development of ProB were mainly carried out by University of Düsseldorf, with some support by the University of Southampton.		The improvements and development of ProB were mainly carried out by University of Düsseldorf, with some support by the University of Southampton.
Line 6:		Line 6:

	New features:		New features:
	* Multi-level animation and validation		* Multi-level animation and validation.
	* B-Motion Studio		* B-Motion Studio.
	* Disprover Support		* Disprover Support.
	* ~~first~~ steps towards test-case generation		* First steps towards test-case generation.

	Improvements:		Improvements:
	* Scalability improvements driven by Siemens and SAP applications		* Scalability improvements driven by Siemens and SAP applications.
	* Using proof information to improve model checking		* Using proof information to improve model checking.

	Other works:		Other works:
	* First steps towards validation of ProB for usage by Siemens in SIL-4 chain		* First steps towards validation of ProB for usage by Siemens in SIL-4 chain.
	* Evaluation against SAT/SMT/BDD-based approaches		* Evaluation against SAT/SMT/BDD-based approaches.

	= Motivations =		= Motivations =