Flows Plug-in - Revision history

imported>Tommy at 17:36, 3 December 2010

2010-12-03T17:36:02Z

← Older revision		Revision as of 17:36, 3 December 2010
Line 17:		Line 17:
	=== Planning ===		=== Planning ===
	The plan is to gather feedback from the users within the Project and encourage the external users to try out the plug-in and provide feedback and feature requests. There are many ideas on the tool extension, in particular using the tool to document event refinement (split, merge, group, refinement diagrams) and provide mechanised patterns for some of the more important cases.		The plan is to gather feedback from the users within the Project and encourage the external users to try out the plug-in and provide feedback and feature requests. There are many ideas on the tool extension, in particular using the tool to document event refinement (split, merge, group, refinement diagrams) and provide mechanised patterns for some of the more important cases.

	~~[[Category:D32 Deliverable]]~~
	~~[[Category:Books]]~~

imported>Alexili at 02:45, 30 November 2010

2010-11-30T02:45:41Z

← Older revision		Revision as of 02:45, 30 November 2010
Line 11:		Line 11:

	=== Available Documentation ===		=== Available Documentation ===
	* An extensive example of the application of the flows in the modelling (the old version) is available to the ~~Deploy~~ Project members as a part of the Bosch cruise control case study.		* An extensive example of the application of the flows in the modelling (the old version) is available to the DEPLOY Project members as a part of the Bosch cruise control case study.
	* There is a wiki page describing the core proof obligations generated by the tool - [[Flows]]		* There is a wiki page describing the core proof obligations generated by the tool - [[Flows]]
	* Tutorial slides available from the project file share		* Tutorial slides available from the project file share

imported>Alexili at 02:44, 30 November 2010

2010-11-30T02:44:12Z

← Older revision		Revision as of 02:44, 30 November 2010
Line 17:		Line 17:
	=== Planning ===		=== Planning ===
	The plan is to gather feedback from the users within the Project and encourage the external users to try out the plug-in and provide feedback and feature requests. There are many ideas on the tool extension, in particular using the tool to document event refinement (split, merge, group, refinement diagrams) and provide mechanised patterns for some of the more important cases.		The plan is to gather feedback from the users within the Project and encourage the external users to try out the plug-in and provide feedback and feature requests. There are many ideas on the tool extension, in particular using the tool to document event refinement (split, merge, group, refinement diagrams) and provide mechanised patterns for some of the more important cases.

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

imported>Alexili at 19:06, 29 November 2010

2010-11-29T19:06:31Z

← Older revision		Revision as of 19:06, 29 November 2010
Line 2:		Line 2:
	Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The Flows plug-in addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover divergencies and deadlocks not already present in the original machine. In other words, the constraining of event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved.		Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The Flows plug-in addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover divergencies and deadlocks not already present in the original machine. In other words, the constraining of event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved.

	The main purpose of the Flows plug-in is to give a modeller a clean and concise view of the control flow aspects of a model without cluttering the model with program counter variables and associated guards and actions. The plug-in is essentially a graphical notation for formulating certain kind of theorems. The new version is to be released in February 2011 and this will include facilities for expressing a wider range of enabledness properties as well as tools for describing event refinement. It is going to address one of the critical shortcomings of the previous version: generation of ~~extremely~~ proof obligations (a large disjunction in a goal comprising several hundreds of terms). The ~~tools~~ is developed by Newcastle University ~~following~~ the requirements and suggestions from Bosch and SAP.		The main purpose of the Flows plug-in is to give a modeller a clean and concise view of the control flow aspects of a model without cluttering the model with program counter variables and associated guards and actions. The plug-in is essentially a graphical notation for formulating certain kind of theorems. The new version is to be released in February 2011 and this will include facilities for expressing a wider range of enabledness properties as well as tools for describing event refinement. It is going to address one of the critical shortcomings of the previous version: generation of unwieldy proof obligations (a large disjunction in a goal comprising several hundreds of terms). The tool is developed by Newcastle University with the requirements and suggestions from Bosch and SAP.

	=== Motivations ===		=== Motivations ===
	The tool was applied by Bosch in the development of the cruise control model to verify deadlock-freedom and liveness properties of the model. Being a sizable case-study, this was an important test for the ideas and techniques behind the plug-in. The general conclusion was that a tool of this kind is essential and the current version should be improved in many directions. This experience has uncovered a rather fundamental issues with the size and complexity of the generated proof obligations. These were the largest theorems ever generated in Rodin and ~~some core platform issues were uncovered as~~ the ~~result~~. It was clear that such proof obligations can never be comfortably handled by Rodin tools (although there were some encouraging results in the application of ProB as a disprover for these kind of proofs) and it was decided that the approach to proof generation requires a complete redesign.		The tool was applied by Bosch in the development of the cruise control model to verify deadlock-freedom and liveness properties of the model. Being a sizable case-study, this was an important test for the ideas and techniques behind the plug-in. The general conclusion was that a tool of this kind is essential and the current version should be improved in many directions. This experience has uncovered a rather fundamental issues with the size and complexity of the generated proof obligations. These were the largest theorems ever generated in Rodin and the only positive aspect is that this helped to stress-test and debug the proof handling facilities of the Rodin. It was clear that such proof obligations can never be comfortably handled by Rodin tools (although there were some encouraging results in the application of ProB as a disprover for these kind of proofs) and it was decided that the approach to proof generation requires a complete redesign.

	=== Choices / Decisions ===		=== Choices / Decisions ===
	The new tool version ~~introducing~~ new ~~forms~~ of diagram structuring ~~primitives~~ to prevent the appearance of ~~very~~ large proof obligations. The typical source of such a proof ~~obligation~~ is demonstrating that an event enables one or more of a long list of events. Technically, the proof would state that the after-state of the event implies the disjunction of the guards of the next events~~. We apply the divide and conquer principle~~. To prevent the appearance of such a disjunction a modeller is encouraged to split the list into a set of sub-models. Each sub-model has a pre- and post-conditions and there are proof obligations demonstrating that all the entry events of the sub-model are enabled when the precondition is satisfied and, symmetrically, every exit event satisfies the sub-model post-condition. Externally, a sub-model appears to be an event with an the precondition as a guard and the postcondition as the set of actions. Although it is more work now for a modeller to produce a flow diagram the extra effort should pay off at the proving stage.		The single most important feature of the new tool version is the introduction of a new form of diagram structuring to prevent the appearance of large proof obligations. The typical source of such proof obligations is demonstrating that an event enables one or more events from a long list of events. Technically, the proof would state that the after-state of the event implies the disjunction of the guards of the next events. To prevent the appearance of such a disjunction a modeller is encouraged to split the list into a set of sub-models. Each sub-model has a pre- and post-conditions and there are proof obligations demonstrating that all the entry events of the sub-model are enabled when the precondition is satisfied and, symmetrically, every exit event satisfies the sub-model post-condition. Externally, a sub-model appears to be a simple atomic event.


	=== Available Documentation ===		=== Available Documentation ===
Line 17:		Line 16:

	=== Planning ===		=== Planning ===
	The plan is to gather feedback from the users within the Project and encourage the external users to try out the plug-in and provide feedback and ~~future~~ requests. There are many ideas on the tool extension, in particular using the tool to document event refinement (split, merge, group, refinement diagrams) and provide mechanised patterns for some of the more important cases.		The plan is to gather feedback from the users within the Project and encourage the external users to try out the plug-in and provide feedback and feature requests. There are many ideas on the tool extension, in particular using the tool to document event refinement (split, merge, group, refinement diagrams) and provide mechanised patterns for some of the more important cases.

imported>Alexili at 18:58, 29 November 2010

2010-11-29T18:58:17Z

← Older revision		Revision as of 18:58, 29 November 2010
Line 1:		Line 1:
			=== Overview ===
			Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The Flows plug-in addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover divergencies and deadlocks not already present in the original machine. In other words, the constraining of event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved.

	~~=== Overview ===~~		The main purpose of the Flows plug-in is to give a modeller a clean and concise view of the control flow aspects of a model without cluttering the model with program counter variables and associated guards and actions. The plug-in is essentially a graphical notation for formulating certain kind of theorems. The new version is to be released in February 2011 and this will include facilities for expressing a wider range of enabledness properties as well as tools for describing event refinement. It is going to address one of the critical shortcomings of the previous version: generation of extremely proof obligations (a large disjunction in a goal comprising several hundreds of terms). The tools is developed by Newcastle University following the requirements and suggestions from Bosch and SAP.
	The ~~flows~~ plug-in ~~allows a modeller to define event ordering constraints using a visual notation. Its main purpose~~ is to give a clean and concise view of ~~model~~ control flow without cluttering the model with program counter variables and associated guards and actions. The plug-in is essentially a graphical notation for formulating certain kind of theorems. The new version is to be released in February 2011 and this will include facilities for expressing a wider range of enabledness properties as well as tools for describing event refinement. It is going to address one of the critical shortcomings of the previous version: generation of extremely proof obligations (a large disjunction in a goal comprising several hundreds of terms). The tools is developed by Newcastle University following the requirements and suggestions from Bosch and SAP.

	=== 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~~.		The tool was applied by Bosch in the development of the cruise control model to verify deadlock-freedom and liveness properties of the model. Being a sizable case-study, this was an important test for the ideas and techniques behind the plug-in. The general conclusion was that a tool of this kind is essential and the current version should be improved in many directions. This experience has uncovered a rather fundamental issues with the size and complexity of the generated proof obligations. These were the largest theorems ever generated in Rodin and some core platform issues were uncovered as the result. It was clear that such proof obligations can never be comfortably handled by Rodin tools (although there were some encouraging results in the application of ProB as a disprover for these kind of proofs) and it was decided that the approach to proof generation requires a complete redesign.

	=== Choices / Decisions ===		=== Choices / Decisions ===
	~~This paragraph shall summarize~~ the ~~decisions (eg~~. ~~design decisions)~~ and ~~justify them~~. ~~Thus~~, ~~it may present~~ the ~~studied solutions~~, ~~through their main advantages~~ and ~~inconvenients,~~ to ~~legitimate~~ the ~~final choices~~.		The new tool version introducing new forms of diagram structuring primitives to prevent the appearance of very large proof obligations. The typical source of such a proof obligation is demonstrating that an event enables one or more of a long list of events. Technically, the proof would state that the after-state of the event implies the disjunction of the guards of the next events. We apply the divide and conquer principle. To prevent the appearance of such a disjunction a modeller is encouraged to split the list into a set of sub-models. Each sub-model has a pre- and post-conditions and there are proof obligations demonstrating that all the entry events of the sub-model are enabled when the precondition is satisfied and, symmetrically, every exit event satisfies the sub-model post-condition. Externally, a sub-model appears to be an event with an the precondition as a guard and the postcondition as the set of actions. Although it is more work now for a modeller to produce a flow diagram the extra effort should pay off at the proving stage.


	=== Available Documentation ===		=== Available Documentation ===
	~~This paragraph shall give pointers to~~ the ~~available wiki pages or related publications. This documentation may contain:~~		* An extensive example of the application of the flows in the modelling (the old version) is available to the Deploy Project members as a part of the Bosch cruise control case study.
	* Requirements.		* There is a wiki page describing the core proof obligations generated by the tool - [[Flows]]
	* Pre-studies (states of the ~~art, proposals, discussions).~~		* Tutorial slides available from the project file share
	* Technical details (~~specifications~~).
	* ~~Teaching materials (tutorials).~~
	* ~~User's guides.~~
	~~A distinction shall be made on the one hand between these different categories, and on~~ the ~~other hand between documentation written for developers and documentation written for end-users.~~

	=== Planning ===		=== Planning ===
	~~This paragraph shall give a timeline~~ and ~~current status~~ (as of ~~28 Jan 2011)~~.		The plan is to gather feedback from the users within the Project and encourage the external users to try out the plug-in and provide feedback and future requests. There are many ideas on the tool extension, in particular using the tool to document event refinement (split, merge, group, refinement diagrams) and provide mechanised patterns for some of the more important cases.

imported>Alexili: New page: === Overview === The flows plug-in allows a modeller to define event ordering constraints using a visual notation. Its main purpose is to give a clean and concise view of model control fl...

2010-11-29T18:21:37Z

New page: === Overview === The flows plug-in allows a modeller to define event ordering constraints using a visual notation. Its main purpose is to give a clean and concise view of model control fl...

New page

=== Overview ===
The flows plug-in allows a modeller to define event ordering constraints using a visual notation. Its main purpose is to give a clean and concise view of model control flow without cluttering the model with program counter variables and associated guards and actions. The plug-in is essentially a graphical notation for formulating certain kind of theorems. The new version is to be released in February 2011 and this will include facilities for expressing a wider range of enabledness properties as well as tools for describing event refinement. It is going to address one of the critical shortcomings of the previous version: generation of extremely proof obligations (a large disjunction in a goal comprising several hundreds of terms). The tools is developed by Newcastle University following the requirements and suggestions from Bosch and SAP.

=== 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.

=== Choices / Decisions ===
This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.

=== Available Documentation ===
This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:
* Requirements.
* Pre-studies (states of the art, proposals, discussions).
* Technical details (specifications).
* Teaching materials (tutorials).
* User's guides.
A distinction shall be made on the one hand between these different categories, and on the other hand between documentation written for developers and documentation written for end-users.

=== Planning ===
This paragraph shall give a timeline and current status (as of 28 Jan 2011).